# Metamath Proof Explorer

## Theorem eu3v

Description: An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994) Replace a nonfreeness hypothesis with a disjoint variable condition on ph , y to reduce axiom usage. (Revised by Wolf Lammen, 29-May-2019)

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

### Proof

Step Hyp Ref Expression
1 df-eu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 df-mo ${⊢}{\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)$
3 2 anbi2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$
4 1 3 bitri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$