# Metamath Proof Explorer

## Theorem 2exeuv

Description: Version of 2exeu with x and y distinct, but not requiring ax-13 . (Contributed by Wolf Lammen, 2-Oct-2023)

Ref Expression
Assertion 2exeuv ${⊢}\left(\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 eumo ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 euex ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 moimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 1 3 syl ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 2euexv ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 4 5 anim12ci ${⊢}\left(\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 df-eu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 6 7 sylibr ${⊢}\left(\exists !{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists !{x}\phantom{\rule{.4em}{0ex}}\exists !{y}\phantom{\rule{.4em}{0ex}}{\phi }$