Theorem 19.42v

Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

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

Proof

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