Theorem difdifdir

Description: Distributive law for class difference. Exercise 4.8 of Stoll p. 16. (Contributed by NM, 18-Aug-2004)

	Ref	Expression
Assertion	difdifdir	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\setminus \left(B\setminus C\right)$$

Proof

Step	Hyp	Ref	Expression
1		dif32	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\setminus B$$
2		invdif	$$⊢\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)=\left(A\setminus C\right)\setminus B$$
3	1 2	eqtr4i	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)$$
4		un0	$$⊢\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \varnothing =\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)$$
5	3 4	eqtr4i	$$⊢\left(A\setminus B\right)\setminus C=\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \varnothing$$
6		indi	$$⊢\left(A\setminus C\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup C\right)=\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \left(\left(A\setminus C\right)\cap C\right)$$
7		disjdif	$$⊢C\cap \left(A\setminus C\right)=\varnothing$$
8		incom	$$⊢C\cap \left(A\setminus C\right)=\left(A\setminus C\right)\cap C$$
9	7 8	eqtr3i	$$⊢\varnothing =\left(A\setminus C\right)\cap C$$
10	9	uneq2i	$$⊢\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \varnothing =\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \left(\left(A\setminus C\right)\cap C\right)$$
11	6 10	eqtr4i	$$⊢\left(A\setminus C\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup C\right)=\left(\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus B\right)\right)\cup \varnothing$$
12	5 11	eqtr4i	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup C\right)$$
13		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus C\right)=C$$
14	13	uneq2i	$$⊢\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus C\right)\right)=\left(\mathrm{V}\setminus B\right)\cup C$$
15		indm	$$⊢\mathrm{V}\setminus \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus C\right)\right)$$
16		invdif	$$⊢B\cap \left(\mathrm{V}\setminus C\right)=B\setminus C$$
17	16	difeq2i	$$⊢\mathrm{V}\setminus \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\mathrm{V}\setminus \left(B\setminus C\right)$$
18	15 17	eqtr3i	$$⊢\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus C\right)\right)=\mathrm{V}\setminus \left(B\setminus C\right)$$
19	14 18	eqtr3i	$$⊢\left(\mathrm{V}\setminus B\right)\cup C=\mathrm{V}\setminus \left(B\setminus C\right)$$
20	19	ineq2i	$$⊢\left(A\setminus C\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup C\right)=\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus \left(B\setminus C\right)\right)$$
21		invdif	$$⊢\left(A\setminus C\right)\cap \left(\mathrm{V}\setminus \left(B\setminus C\right)\right)=\left(A\setminus C\right)\setminus \left(B\setminus C\right)$$
22	12 20 21	3eqtri	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\setminus \left(B\setminus C\right)$$