Metamath Proof Explorer


Theorem xpdisj1

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

Ref Expression
Assertion xpdisj1 AB=A×CB×D=

Proof

Step Hyp Ref Expression
1 xpeq1 AB=AB×CD=×CD
2 inxp A×CB×D=AB×CD
3 0xp ×CD=
4 3 eqcomi =×CD
5 1 2 4 3eqtr4g AB=A×CB×D=