Metamath Proof Explorer

Theorem xpindi

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

Ref Expression
Assertion xpindi 
|- ( A X. ( B i^i C ) ) = ( ( A X. B ) i^i ( A X. C ) )

Proof

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