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

Proof

Step	Hyp	Ref	Expression
1		difxp	$$⊢\left(A\times B\right)\setminus \left(A\times C\right)=\left(\left(A\setminus A\right)\times B\right)\cup \left(A\times \left(B\setminus C\right)\right)$$
2		difid	$$⊢A\setminus A=\varnothing$$
3	2	xpeq1i	$$⊢\left(A\setminus A\right)\times B=\varnothing \times B$$
4		0xp	$$⊢\varnothing \times B=\varnothing$$
5	3 4	eqtri	$$⊢\left(A\setminus A\right)\times B=\varnothing$$
6	5	uneq1i	$$⊢\left(\left(A\setminus A\right)\times B\right)\cup \left(A\times \left(B\setminus C\right)\right)=\varnothing \cup \left(A\times \left(B\setminus C\right)\right)$$
7		uncom	$$⊢\varnothing \cup \left(A\times \left(B\setminus C\right)\right)=\left(A\times \left(B\setminus C\right)\right)\cup \varnothing$$
8		un0	$$⊢\left(A\times \left(B\setminus C\right)\right)\cup \varnothing =A\times \left(B\setminus C\right)$$
9	7 8	eqtri	$$⊢\varnothing \cup \left(A\times \left(B\setminus C\right)\right)=A\times \left(B\setminus C\right)$$
10	1 6 9	3eqtrri	$$⊢A\times \left(B\setminus C\right)=\left(A\times B\right)\setminus \left(A\times C\right)$$