Theorem elsng

Description: There is exactly one element in a singleton. Exercise 2 of TakeutiZaring p. 15 (generalized). (Contributed by NM, 13-Sep-1995) (Proof shortened by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	elsng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐵 ↔ 𝑦 = 𝐵 ) )
2		eqeq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝐴 = 𝐵 ) )
3		df-sn	⊢ { 𝐵 } = { 𝑥 ∣ 𝑥 = 𝐵 }
4	1 2 3	elab2gw	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )