Theorem difundi

Description: Distributive law for class difference. Theorem 39 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

	Ref	Expression
Assertion	difundi	$$⊢A\setminus \left(B\cup C\right)=\left(A\setminus B\right)\cap \left(A\setminus C\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfun3	$$⊢B\cup C=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)$$
2	1	difeq2i	$$⊢A\setminus \left(B\cup C\right)=A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
3		inindi	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cap \left(A\cap \left(\mathrm{V}\setminus C\right)\right)$$
4		dfin2	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)=A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)$$
5		invdif	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus B$$
6		invdif	$$⊢A\cap \left(\mathrm{V}\setminus C\right)=A\setminus C$$
7	5 6	ineq12i	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cap \left(A\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\setminus B\right)\cap \left(A\setminus C\right)$$
8	3 4 7	3eqtr3i	$$⊢A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)\right)=\left(A\setminus B\right)\cap \left(A\setminus C\right)$$
9	2 8	eqtri	$$⊢A\setminus \left(B\cup C\right)=\left(A\setminus B\right)\cap \left(A\setminus C\right)$$