Theorem 19.3

Description: 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)

	Ref	Expression
Hypothesis	19.3.1	$$⊢Ⅎx\phi$$
Assertion	19.3	$$⊢\forall x\phi \leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		19.3.1	$$⊢Ⅎx\phi$$
2		sp	$$⊢\forall x\phi \to \phi$$
3	1	nf5ri	$$⊢\phi \to \forall x\phi$$
4	2 3	impbii	$$⊢\forall x\phi \leftrightarrow \phi$$