Theorem r2exf

Description: Double restricted existential quantification. For a version based on fewer axioms see r2ex . (Contributed by Mario Carneiro, 14-Oct-2016) Use r2exlem . (Revised by Wolf Lammen, 10-Jan-2020)

	Ref	Expression
Hypothesis	r2exf.1	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	r2exf	$$⊢\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		r2exf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2	1	r2alf	$$⊢\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)$$
3	2	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)$$