# Metamath Proof Explorer

## 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 }↔{\psi }\right)$
Assertion rexxp ${⊢}\exists {x}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

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