Theorem dif32

Description: Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		uncom	$$⊢B\cup C=C\cup B$$
2	1	difeq2i	$$⊢A\setminus \left(B\cup C\right)=A\setminus \left(C\cup B\right)$$
3		difun1	$$⊢A\setminus \left(B\cup C\right)=\left(A\setminus B\right)\setminus C$$
4		difun1	$$⊢A\setminus \left(C\cup B\right)=\left(A\setminus C\right)\setminus B$$
5	2 3 4	3eqtr3i	$$⊢\left(A\setminus B\right)\setminus C=\left(A\setminus C\right)\setminus B$$