Metamath Proof Explorer


Theorem xpdisj2

Description: Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004)

Ref Expression
Assertion xpdisj2 A B = C × A D × B =

Proof

Step Hyp Ref Expression
1 xpeq2 A B = C D × A B = C D ×
2 inxp C × A D × B = C D × A B
3 xp0 C D × =
4 3 eqcomi = C D ×
5 1 2 4 3eqtr4g A B = C × A D × B =