This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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		df-sn	⊢ { 𝐵 } = { 𝑥 ∣ 𝑥 = 𝐵 }
3	1 2	elab2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )