Theorem rexxp

Description: Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995) (Revised by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypothesis	ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rexxp	$$⊢\exists x\in \left(A\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	$$⊢x=⟨y,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
2		iunxpconst	$$⊢\bigcup _{y\in A}\left(\left\{y\right\}\times B\right)=A\times B$$
3	2	rexeqi	$$⊢\exists x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \exists x\in \left(A\times B\right)\phi$$
4	1	rexiunxp	$$⊢\exists x\in \bigcup _{y\in A}\left(\left\{y\right\}\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$
5	3 4	bitr3i	$$⊢\exists x\in \left(A\times B\right)\phi \leftrightarrow \exists y\in A\exists z\in B\psi$$