This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 × 𝐵 ) ∖ ( 𝐴 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 difxp ⊢ ( ( 𝐴 × 𝐵 ) ∖ ( 𝐴 × 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐴 ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) )
2 difid ⊢ ( 𝐴 ∖ 𝐴 ) = ∅
3 2 xpeq1i ⊢ ( ( 𝐴 ∖ 𝐴 ) × 𝐵 ) = ( ∅ × 𝐵 )
4 0xp ⊢ ( ∅ × 𝐵 ) = ∅
5 3 4 eqtri ⊢ ( ( 𝐴 ∖ 𝐴 ) × 𝐵 ) = ∅
6 5 uneq1i ⊢ ( ( ( 𝐴 ∖ 𝐴 ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) ) = ( ∅ ∪ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) )
7 uncom ⊢ ( ∅ ∪ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) ) = ( ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) ∪ ∅ )
8 un0 ⊢ ( ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) ∪ ∅ ) = ( 𝐴 × ( 𝐵 ∖ 𝐶 ) )
9 7 8 eqtri ⊢ ( ∅ ∪ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) ) = ( 𝐴 × ( 𝐵 ∖ 𝐶 ) )
10 1 6 9 3eqtrri ⊢ ( 𝐴 × ( 𝐵 ∖ 𝐶 ) ) = ( ( 𝐴 × 𝐵 ) ∖ ( 𝐴 × 𝐶 ) )