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 
|- ( ( A i^i B ) X. C ) = ( ( A X. C ) i^i ( B X. C ) )

Proof

Step Hyp Ref Expression
1 inxp 
 |-  ( ( A X. C ) i^i ( B X. C ) ) = ( ( A i^i B ) X. ( C i^i C ) )
2 inidm 
 |-  ( C i^i C ) = C
3 2 xpeq2i 
 |-  ( ( A i^i B ) X. ( C i^i C ) ) = ( ( A i^i B ) X. C )
4 1 3 eqtr2i 
 |-  ( ( A i^i B ) X. C ) = ( ( A X. C ) i^i ( B X. C ) )