Theorem difindi

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

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

Proof

Step	Hyp	Ref	Expression
1		dfin3	$$⊢B\cap C=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus C\right)\right)$$
2	1	difeq2i	$$⊢A\setminus \left(B\cap C\right)=A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus C\right)\right)\right)$$
3		indi	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus C\right)\right)=\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cup \left(A\cap \left(\mathrm{V}\setminus C\right)\right)$$
4		dfin2	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus C\right)\right)=A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cup \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	uneq12i	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cup \left(A\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\setminus B\right)\cup \left(A\setminus C\right)$$
8	3 4 7	3eqtr3i	$$⊢A\setminus \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus B\right)\cup \left(\mathrm{V}\setminus C\right)\right)\right)=\left(A\setminus B\right)\cup \left(A\setminus C\right)$$
9	2 8	eqtri	$$⊢A\setminus \left(B\cap C\right)=\left(A\setminus B\right)\cup \left(A\setminus C\right)$$