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

Proof

Step	Hyp	Ref	Expression
1		difxp	⊢ ( ( 𝐴 × 𝐶 ) ∖ ( 𝐵 × 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐵 ) × 𝐶 ) ∪ ( 𝐴 × ( 𝐶 ∖ 𝐶 ) ) )
2		difid	⊢ ( 𝐶 ∖ 𝐶 ) = ∅
3	2	xpeq2i	⊢ ( 𝐴 × ( 𝐶 ∖ 𝐶 ) ) = ( 𝐴 × ∅ )
4		xp0	⊢ ( 𝐴 × ∅ ) = ∅
5	3 4	eqtri	⊢ ( 𝐴 × ( 𝐶 ∖ 𝐶 ) ) = ∅
6	5	uneq2i	⊢ ( ( ( 𝐴 ∖ 𝐵 ) × 𝐶 ) ∪ ( 𝐴 × ( 𝐶 ∖ 𝐶 ) ) ) = ( ( ( 𝐴 ∖ 𝐵 ) × 𝐶 ) ∪ ∅ )
7		un0	⊢ ( ( ( 𝐴 ∖ 𝐵 ) × 𝐶 ) ∪ ∅ ) = ( ( 𝐴 ∖ 𝐵 ) × 𝐶 )
8	1 6 7	3eqtrri	⊢ ( ( 𝐴 ∖ 𝐵 ) × 𝐶 ) = ( ( 𝐴 × 𝐶 ) ∖ ( 𝐵 × 𝐶 ) )