Metamath Proof Explorer


Theorem xpindir

Description: Distributive law for Cartesian product over intersection. Similar to Theorem 102 of Suppes p. 52. (Contributed by NM, 26-Sep-2004)

Ref Expression
Assertion xpindir AB×C=A×CB×C

Proof

Step Hyp Ref Expression
1 inxp A×CB×C=AB×CC
2 inidm CC=C
3 2 xpeq2i AB×CC=AB×C
4 1 3 eqtr2i AB×C=A×CB×C