Metamath Proof Explorer

Theorem difxp1

Description: Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013) (Revised by Mario Carneiro, 26-Jun-2014)

Ref Expression
Assertion difxp1 
|- ( ( A \ B ) X. C ) = ( ( A X. C ) \ ( B X. C ) )

Proof

Step Hyp Ref Expression
1 difxp 
 |-  ( ( A X. C ) \ ( B X. C ) ) = ( ( ( A \ B ) X. C ) u. ( A X. ( C \ C ) ) )
2 difid 
 |-  ( C \ C ) = (/)
3 2 xpeq2i 
 |-  ( A X. ( C \ C ) ) = ( A X. (/) )
4 xp0 
 |-  ( A X. (/) ) = (/)
5 3 4 eqtri 
 |-  ( A X. ( C \ C ) ) = (/)
6 5 uneq2i 
 |-  ( ( ( A \ B ) X. C ) u. ( A X. ( C \ C ) ) ) = ( ( ( A \ B ) X. C ) u. (/) )
7 un0 
 |-  ( ( ( A \ B ) X. C ) u. (/) ) = ( ( A \ B ) X. C )
8 1 6 7 3eqtrri 
 |-  ( ( A \ B ) X. C ) = ( ( A X. C ) \ ( B X. C ) )