Theorem difindir

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

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

Proof

Step	Hyp	Ref	Expression
1		inindir	$$⊢\left(A\cap B\right)\cap \left(\mathrm{V}\setminus C\right)=\left(A\cap \left(\mathrm{V}\setminus C\right)\right)\cap \left(B\cap \left(\mathrm{V}\setminus C\right)\right)$$
2		invdif	$$⊢\left(A\cap B\right)\cap \left(\mathrm{V}\setminus C\right)=\left(A\cap 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	ineq12i	$$⊢\left(A\cap \left(\mathrm{V}\setminus C\right)\right)\cap \left(B\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\setminus C\right)\cap \left(B\setminus C\right)$$
6	1 2 5	3eqtr3i	$$⊢\left(A\cap B\right)\setminus C=\left(A\setminus C\right)\cap \left(B\setminus C\right)$$