Theorem eusn

Description: Two ways to express " A is a singleton". (Contributed by NM, 30-Oct-2010)

	Ref	Expression
Assertion	eusn	$$⊢\exists !xx\in A\leftrightarrow \exists xA=\left\{x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		euabsn	$$⊢\exists !xx\in A\leftrightarrow \exists x\left\{x|x\in A\right\}=\left\{x\right\}$$
2		abid2	$$⊢\left\{x|x\in A\right\}=A$$
3	2	eqeq1i	$$⊢\left\{x|x\in A\right\}=\left\{x\right\}\leftrightarrow A=\left\{x\right\}$$
4	3	exbii	$$⊢\exists x\left\{x|x\in A\right\}=\left\{x\right\}\leftrightarrow \exists xA=\left\{x\right\}$$
5	1 4	bitri	$$⊢\exists !xx\in A\leftrightarrow \exists xA=\left\{x\right\}$$