Theorem reean

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 27-Oct-2010) (Proof shortened by Andrew Salmon, 30-May-2011)

	Ref	Expression
Hypotheses	reean.1	$$⊢Ⅎy\phi$$
	reean.2	$$⊢Ⅎx\psi$$
Assertion	reean	$$⊢\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		reean.1	$$⊢Ⅎy\phi$$
2		reean.2	$$⊢Ⅎx\psi$$
3		nfv	$$⊢Ⅎyx\in A$$
4	3 1	nfan	$$⊢Ⅎy\left(x\in A\wedge \phi \right)$$
5		nfv	$$⊢Ⅎxy\in B$$
6	5 2	nfan	$$⊢Ⅎx\left(y\in B\wedge \psi \right)$$
7	4 6	eean	$$⊢\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)$$
8	7	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)$$