Theorem difun1

Description: A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		inass	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cap \left(\mathrm{V}\setminus C\right)=A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)$$
2		invdif	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cap \left(\mathrm{V}\setminus C\right)=\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\setminus C$$
3	1 2	eqtr3i	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)=\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\setminus C$$
4		undm	$$⊢\mathrm{V}\setminus \left(B\cup C\right)=\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)$$
5	4	ineq2i	$$⊢A\cap \left(\mathrm{V}\setminus \left(B\cup C\right)\right)=A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)$$
6		invdif	$$⊢A\cap \left(\mathrm{V}\setminus \left(B\cup C\right)\right)=A\setminus \left(B\cup C\right)$$
7	5 6	eqtr3i	$$⊢A\cap \left(\left(\mathrm{V}\setminus B\right)\cap \left(\mathrm{V}\setminus C\right)\right)=A\setminus \left(B\cup C\right)$$
8	3 7	eqtr3i	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\setminus C=A\setminus \left(B\cup C\right)$$
9		invdif	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus B$$
10	9	difeq1i	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\setminus C=\left(A\setminus B\right)\setminus C$$
11	8 10	eqtr3i	$$⊢A\setminus \left(B\cup C\right)=\left(A\setminus B\right)\setminus C$$