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	$$⊢\left(A\setminus B\right)\times C=\left(A\times C\right)\setminus \left(B\times C\right)$$

Proof

Step	Hyp	Ref	Expression
1		difxp	$$⊢\left(A\times C\right)\setminus \left(B\times C\right)=\left(\left(A\setminus B\right)\times C\right)\cup \left(A\times \left(C\setminus C\right)\right)$$
2		difid	$$⊢C\setminus C=\varnothing$$
3	2	xpeq2i	$$⊢A\times \left(C\setminus C\right)=A\times \varnothing$$
4		xp0	$$⊢A\times \varnothing =\varnothing$$
5	3 4	eqtri	$$⊢A\times \left(C\setminus C\right)=\varnothing$$
6	5	uneq2i	$$⊢\left(\left(A\setminus B\right)\times C\right)\cup \left(A\times \left(C\setminus C\right)\right)=\left(\left(A\setminus B\right)\times C\right)\cup \varnothing$$
7		un0	$$⊢\left(\left(A\setminus B\right)\times C\right)\cup \varnothing =\left(A\setminus B\right)\times C$$
8	1 6 7	3eqtrri	$$⊢\left(A\setminus B\right)\times C=\left(A\times C\right)\setminus \left(B\times C\right)$$