Theorem r19.42v

Description: Restricted quantifier version of 19.42v (see also 19.42 ). (Contributed by NM, 27-May-1998)

	Ref	Expression
Assertion	r19.42v	|- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		r19.41v	|- ( E. x e. A ( ps /\ ph ) <-> ( E. x e. A ps /\ ph ) )
2		ancom	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
3	2	rexbii	|- ( E. x e. A ( ph /\ ps ) <-> E. x e. A ( ps /\ ph ) )
4		ancom	|- ( ( ph /\ E. x e. A ps ) <-> ( E. x e. A ps /\ ph ) )
5	1 3 4	3bitr4i	|- ( E. x e. A ( ph /\ ps ) <-> ( ph /\ E. x e. A ps ) )