Theorem indif1

Description: Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		indif2	$$⊢B\cap \left(A\setminus C\right)=\left(B\cap A\right)\setminus C$$
2		incom	$$⊢B\cap \left(A\setminus C\right)=\left(A\setminus C\right)\cap B$$
3		incom	$$⊢B\cap A=A\cap B$$
4	3	difeq1i	$$⊢\left(B\cap A\right)\setminus C=\left(A\cap B\right)\setminus C$$
5	1 2 4	3eqtr3i	$$⊢\left(A\setminus C\right)\cap B=\left(A\cap B\right)\setminus C$$