Theorem reeanv

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999)

	Ref	Expression
Assertion	reeanv	|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		exdistrv	|- ( E. x E. y ( ( x e. A /\ ph ) /\ ( y e. B /\ ps ) ) <-> ( E. x ( x e. A /\ ph ) /\ E. y ( y e. B /\ ps ) ) )
2	1	reeanlem	|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )