Theorem undif1 4423

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

Assertion

Ref	Expression
undif1	⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Proof of Theorem undif1

Step	Hyp	Ref	Expression
1		undir 4234	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4226	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4111	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4105	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4422	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2754	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4164	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4345	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2754	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2762	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1541  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281

This theorem is referenced by:  undif2  4424  undifr  4430  unidif0  5296  sofld  6134  fresaun  6694  ralxpmap  8820  enp1ilem  9162  difinf  9195  pwfilem  9202  infdif  10099  fin23lem11  10208  fin1a2lem13  10303  axcclem  10348  ttukeylem1  10400  ttukeylem7  10406  fpwwe2lem12  10533  hashbclem  14359  incexclem  15743  ramub1lem1  16938  ramub1lem2  16939  isstruct2  17060  setsdm  17081  mrieqvlemd  17535  mreexmrid  17549  islbs3  21092  lbsextlem4  21098  basdif0  22868  bwth  23325  locfincmp  23441  cldsubg  24026  nulmbl2  25464  volinun  25474  limcdif  25804  ellimc2  25805  limcmpt2  25812  dvreslem  25837  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  lhop  25948  plyeq0  26143  rlimcnp  26902  difeq  32498  ffsrn  32711  symgcom2  33053  esumpad2  34069  measunl  34229  subfacp1lem1  35223  cvmscld  35317  pibt2  37459  stoweidlem44  46090