Metamath Proof Explorer

Theorem xpsndisj

Description: Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004)

Ref Expression
Assertion xpsndisj 
|- ( B =/= D -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )

Proof

Step Hyp Ref Expression
1 disjsn2 
 |-  ( B =/= D -> ( { B } i^i { D } ) = (/) )
2 xpdisj2 
 |-  ( ( { B } i^i { D } ) = (/) -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )
3 1 2 syl 
 |-  ( B =/= D -> ( ( A X. { B } ) i^i ( C X. { D } ) ) = (/) )