Metamath Proof Explorer

Theorem disjsn2

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

Ref Expression
Assertion disjsn2 
|- ( A =/= B -> ( { A } i^i { B } ) = (/) )

Proof

Step Hyp Ref Expression
1 elsni 
 |-  ( B e. { A } -> B = A )
2 1 eqcomd 
 |-  ( B e. { A } -> A = B )
3 2 necon3ai 
 |-  ( A =/= B -> -. B e. { A } )
4 disjsn 
 |-  ( ( { A } i^i { B } ) = (/) <-> -. B e. { A } )
5 3 4 sylibr 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )