# Metamath Proof Explorer

## Theorem sniota

Description: A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion sniota ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left\{{x}|{\phi }\right\}=\left\{\left(\iota {x}|{\phi }\right)\right\}$

### Proof

Step Hyp Ref Expression
1 nfeu1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfab1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{x}|{\phi }\right\}$
3 nfiota1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left(\iota {x}|{\phi }\right)$
4 3 nfsn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{\left(\iota {x}|{\phi }\right)\right\}$
5 iota1 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\phi }↔\left(\iota {x}|{\phi }\right)={x}\right)$
6 eqcom ${⊢}\left(\iota {x}|{\phi }\right)={x}↔{x}=\left(\iota {x}|{\phi }\right)$
7 5 6 syl6bb ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({\phi }↔{x}=\left(\iota {x}|{\phi }\right)\right)$
8 abid ${⊢}{x}\in \left\{{x}|{\phi }\right\}↔{\phi }$
9 velsn ${⊢}{x}\in \left\{\left(\iota {x}|{\phi }\right)\right\}↔{x}=\left(\iota {x}|{\phi }\right)$
10 7 8 9 3bitr4g ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({x}\in \left\{{x}|{\phi }\right\}↔{x}\in \left\{\left(\iota {x}|{\phi }\right)\right\}\right)$
11 1 2 4 10 eqrd ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left\{{x}|{\phi }\right\}=\left\{\left(\iota {x}|{\phi }\right)\right\}$