# Metamath Proof Explorer

## Theorem euabsneu

Description: Another way to express existential uniqueness of a wff ph : its associated class abstraction { x | ph } is a singleton. Variant of euabsn2 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion euabsneu ${⊢}\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 mosneq ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}\right\}=\left\{{x}|{\phi }\right\}$
2 eqcom ${⊢}\left\{{y}\right\}=\left\{{x}|{\phi }\right\}↔\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$
3 2 mobii ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{y}\right\}=\left\{{x}|{\phi }\right\}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$
4 1 3 mpbi ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$
5 4 biantru ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right)$
6 euabsn2 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$
7 df-eu ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\wedge {\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}\right)$
8 5 6 7 3bitr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}=\left\{{y}\right\}$