# Metamath Proof Explorer

## Theorem exopxfr

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis exopxfr.1 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
Assertion exopxfr ${⊢}\exists {x}\in \left(\mathrm{V}×\mathrm{V}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 exopxfr.1 ${⊢}{x}=⟨{y},{z}⟩\to \left({\phi }↔{\psi }\right)$
2 1 rexxp ${⊢}\exists {x}\in \left(\mathrm{V}×\mathrm{V}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\psi }$
3 rexv ${⊢}\exists {y}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\psi }$
4 rexv ${⊢}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {z}\phantom{\rule{.4em}{0ex}}{\psi }$
5 4 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\in \mathrm{V}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{\psi }$
6 2 3 5 3bitri ${⊢}\exists {x}\in \left(\mathrm{V}×\mathrm{V}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{\psi }$