# Metamath Proof Explorer

## Theorem dfmo

Description: Rederive df-mo from the old definition moeu . (Contributed by Wolf Lammen, 27-May-2019) (Proof modification is discouraged.) Use df-mo instead. (New usage is discouraged.)

Ref Expression
Assertion dfmo ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\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 eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
3 2 imbi2i ${⊢}\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 {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
4 dfmoeu ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
5 1 3 4 3bitri ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$