Theorem undif1

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif ). Theorem 35 of Suppes p. 29. (Contributed by NM, 19-May-1998)

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

Proof

Step	Hyp	Ref	Expression
1		undir	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cup B=\left(A\cup B\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup B\right)$$
2		invdif	$$⊢A\cap \left(\mathrm{V}\setminus B\right)=A\setminus B$$
3	2	uneq1i	$$⊢\left(A\cap \left(\mathrm{V}\setminus B\right)\right)\cup B=\left(A\setminus B\right)\cup B$$
4		uncom	$$⊢\left(\mathrm{V}\setminus B\right)\cup B=B\cup \left(\mathrm{V}\setminus B\right)$$
5		unvdif	$$⊢B\cup \left(\mathrm{V}\setminus B\right)=\mathrm{V}$$
6	4 5	eqtri	$$⊢\left(\mathrm{V}\setminus B\right)\cup B=\mathrm{V}$$
7	6	ineq2i	$$⊢\left(A\cup B\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup B\right)=\left(A\cup B\right)\cap \mathrm{V}$$
8		inv1	$$⊢\left(A\cup B\right)\cap \mathrm{V}=A\cup B$$
9	7 8	eqtri	$$⊢\left(A\cup B\right)\cap \left(\left(\mathrm{V}\setminus B\right)\cup B\right)=A\cup B$$
10	1 3 9	3eqtr3i	$$⊢\left(A\setminus B\right)\cup B=A\cup B$$