Theorem reeanv

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

	Ref	Expression
Assertion	reeanv	$$⊢\exists x\in A\exists y\in B\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\in A\phi \wedge \exists y\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exdistrv	$$⊢\exists x\exists y\left(\left(x\in A\wedge \phi \right)\wedge \left(y\in B\wedge \psi \right)\right)\leftrightarrow \left(\exists x\left(x\in A\wedge \phi \right)\wedge \exists y\left(y\in B\wedge \psi \right)\right)$$
2	1	reeanlem	$$⊢\exists x\in A\exists y\in B\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists x\in A\phi \wedge \exists y\in B\psi \right)$$