Theorem 19.42

Description: Theorem 19.42 of Margaris p. 90. See 19.42v for a version requiring fewer axioms. See exan for an immediate version. (Contributed by NM, 18-Aug-1993)

	Ref	Expression
Hypothesis	19.42.1	|- F/ x ph
Assertion	19.42	|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.42.1	|- F/ x ph
2	1	19.41	|- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
3		exancom	|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
4		ancom	|- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) )
5	2 3 4	3bitr4i	|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )