Theorem indifcom

Description: Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013)

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

Proof

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