Theorem elsni

Description: There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994)

	Ref	Expression
Assertion	elsni	⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elsng	⊢ ( 𝐴 ∈ { 𝐵 } → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )
2	1	ibi	⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )