# Metamath Proof Explorer

## Theorem 2exsb

Description: An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005) (Proof shortened by Wolf Lammen, 30-Sep-2018)

Ref Expression
Assertion 2exsb ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={z}\wedge {y}={w}\right)\to {\phi }\right)$

### Proof

Step Hyp Ref Expression
1 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
3 1 2 2sb8ev ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]\left[{w}/{y}\right]{\phi }$
4 2sb6 ${⊢}\left[{z}/{x}\right]\left[{w}/{y}\right]{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={z}\wedge {y}={w}\right)\to {\phi }\right)$
5 4 2exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]\left[{w}/{y}\right]{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={z}\wedge {y}={w}\right)\to {\phi }\right)$
6 3 5 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}={z}\wedge {y}={w}\right)\to {\phi }\right)$