Theorem euabsn

Description: Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Assertion	euabsn	$$⊢\exists !x\phi \leftrightarrow \exists x\left\{x|\phi \right\}=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		euabsn2	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
2		nfv	$$⊢Ⅎy\left\{x|\phi \right\}=\left\{x\right\}$$
3		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
4	3	nfeq1	$$⊢Ⅎx\left\{x|\phi \right\}=\left\{y\right\}$$
5		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
6	5	eqeq2d	$$⊢x=y\to \left(\left\{x|\phi \right\}=\left\{x\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{y\right\}\right)$$
7	2 4 6	cbvexv1	$$⊢\exists x\left\{x|\phi \right\}=\left\{x\right\}\leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
8	1 7	bitr4i	$$⊢\exists !x\phi \leftrightarrow \exists x\left\{x|\phi \right\}=\left\{x\right\}$$