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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )