Theorem difundir

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		indir	$$⊢\left(A\cup B\right)\cap \left(\mathrm{V}\setminus C\right)=\left(A\cap \left(\mathrm{V}\setminus C\right)\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)$$
2		invdif	$$⊢\left(A\cup B\right)\cap \left(\mathrm{V}\setminus C\right)=\left(A\cup B\right)\setminus C$$
3		invdif	$$⊢A\cap \left(\mathrm{V}\setminus C\right)=A\setminus C$$
4		invdif	$$⊢B\cap \left(\mathrm{V}\setminus C\right)=B\setminus C$$
5	3 4	uneq12i	$$⊢\left(A\cap \left(\mathrm{V}\setminus C\right)\right)\cup \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\setminus C\right)\cup \left(B\setminus C\right)$$
6	1 2 5	3eqtr3i	$$⊢\left(A\cup B\right)\setminus C=\left(A\setminus C\right)\cup \left(B\setminus C\right)$$