# Metamath Proof Explorer

## Theorem euabsn2

Description: Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Assertion euabsn2 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$

### Proof

Step Hyp Ref Expression
1 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)$
2 absn ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
3 2 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
4 1 3 bitr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$