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

Metamath Proof Explorer

Theorem disjsn2

Description: Two distinct singletons are disjoint. (Contributed by NM, 25-May-1998)

Ref Expression
Assertion disjsn2 ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )

Proof

Step Hyp Ref Expression
1 elsni ⊢ ( 𝐵 ∈ { 𝐴 } → 𝐵 = 𝐴 )
2 1 eqcomd ⊢ ( 𝐵 ∈ { 𝐴 } → 𝐴 = 𝐵 )
3 2 necon3ai ⊢ ( 𝐴 ≠ 𝐵 → ¬ 𝐵 ∈ { 𝐴 } )
4 disjsn ⊢ ( ( { 𝐴 } ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ { 𝐴 } )
5 3 4 sylibr ⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )