# Metamath Proof Explorer

## Theorem moeu

Description: Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995) This used to be the definition of the at-most-one quantifier, while df-mo was then proved as dfmo . (Revised by BJ, 30-Sep-2022)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 moabs ${⊢}{\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 exmoeub ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 2 pm5.74i ${⊢}\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 }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
4 1 3 bitri ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$