Theorem eusn

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

	Ref	Expression
Assertion	eusn	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		euabsn	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } )
2		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
3	2	eqeq1i	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } ↔ 𝐴 = { 𝑥 } )
4	3	exbii	⊢ ( ∃ 𝑥 { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
5	1 4	bitri	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )