Theorem 19.36

Description: Theorem 19.36 of Margaris p. 90. See 19.36v for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993)

	Ref	Expression
Hypothesis	19.36.1	|- F/ x ps
Assertion	19.36	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.36.1	|- F/ x ps
2		19.35	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
3	1	19.9	|- ( E. x ps <-> ps )
4	3	imbi2i	|- ( ( A. x ph -> E. x ps ) <-> ( A. x ph -> ps ) )
5	2 4	bitri	|- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) )