# Metamath Proof Explorer

## Theorem bj-moeub

Description: Uniqueness is equivalent to existence being equivalent to unique existence. (Contributed by BJ, 14-Oct-2022)

Ref Expression
Assertion bj-moeub ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 moeu ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 euex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 impbi ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left(\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
4 2 3 mpi ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 biimp ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 4 5 impbii ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 1 6 bitri ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$