Theorem 19.3

A wff may be quantified with a variable not free in it. Version of 19.9 with a universal quantifier. Theorem 19.3 of [Margaris] p. 89. See 19.3v for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypothesis
19.3.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \varphi \)
Proof
l0
sp
19.3.1
nf5ri _
impbii l0 _