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