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\phi \to \left\{x|\phi \right\}=\left\{\left(\iota x|\phi \right)\right\}$$

Proof

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