Description: There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | elsni | ⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsng | ⊢ ( 𝐴 ∈ { 𝐵 } → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) ) | |
2 | 1 | ibi | ⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 ) |