Theorem r2ex

Description: Double restricted existential quantification. (Contributed by NM, 11-Nov-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020)

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

Proof

Step	Hyp	Ref	Expression
1		r2al	$$⊢\forall x\in A\forall y\in B\neg \phi \leftrightarrow \forall x\forall y\left(\left(x\in A\wedge y\in B\right)\to \neg \phi \right)$$
2	1	r2exlem	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)$$