Theorem eusn

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

	Ref	Expression
Assertion	eusn	|- ( E! x x e. A <-> E. x A = { x } )

Proof

Step	Hyp	Ref	Expression
1		euabsn	|- ( E! x x e. A <-> E. x { x | x e. A } = { x } )
2		abid2	|- { x | x e. A } = A
3	2	eqeq1i	|- ( { x | x e. A } = { x } <-> A = { x } )
4	3	exbii	|- ( E. x { x | x e. A } = { x } <-> E. x A = { x } )
5	1 4	bitri	|- ( E! x x e. A <-> E. x A = { x } )