Metamath Proof Explorer

Theorem xp01disj

Description: Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007)

Ref Expression
Assertion xp01disj 
|- ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/)

Proof

Step Hyp Ref Expression
1 1n0 
 |-  1o =/= (/)
2 1 necomi 
 |-  (/) =/= 1o
3 xpsndisj 
 |-  ( (/) =/= 1o -> ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/) )
4 2 3 ax-mp 
 |-  ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/)