Metamath Proof Explorer

Theorem difxp2

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

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

Proof

Step Hyp Ref Expression
1 difxp 
 |-  ( ( A X. B ) \ ( A X. C ) ) = ( ( ( A \ A ) X. B ) u. ( A X. ( B \ C ) ) )
2 difid 
 |-  ( A \ A ) = (/)
3 2 xpeq1i 
 |-  ( ( A \ A ) X. B ) = ( (/) X. B )
4 0xp 
 |-  ( (/) X. B ) = (/)
5 3 4 eqtri 
 |-  ( ( A \ A ) X. B ) = (/)
6 5 uneq1i 
 |-  ( ( ( A \ A ) X. B ) u. ( A X. ( B \ C ) ) ) = ( (/) u. ( A X. ( B \ C ) ) )
7 uncom 
 |-  ( (/) u. ( A X. ( B \ C ) ) ) = ( ( A X. ( B \ C ) ) u. (/) )
8 un0 
 |-  ( ( A X. ( B \ C ) ) u. (/) ) = ( A X. ( B \ C ) )
9 7 8 eqtri 
 |-  ( (/) u. ( A X. ( B \ C ) ) ) = ( A X. ( B \ C ) )
10 1 6 9 3eqtrri 
 |-  ( A X. ( B \ C ) ) = ( ( A X. B ) \ ( A X. C ) )