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	|- F/ x ph
Assertion	19.3	|- ( A. x ph <-> ph )

Proof

Step	Hyp	Ref	Expression
1		19.3.1	|- F/ x ph
2		sp	|- ( A. x ph -> ph )
3	1	nf5ri	|- ( ph -> A. x ph )
4	2 3	impbii	|- ( A. x ph <-> ph )