Theorem undif1 4406

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4402). 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 4207	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4199	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4089	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4083	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4405	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2766	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4140	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4325	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2766	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2774	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1539  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  undif2  4407  unidif0  5277  pwundifOLD  5477  sofld  6079  fresaun  6629  ralxpmap  8642  pwfilem  8922  enp1ilem  8981  difinf  9014  pwfilemOLD  9043  infdif  9896  fin23lem11  10004  fin1a2lem13  10099  axcclem  10144  ttukeylem1  10196  ttukeylem7  10202  fpwwe2lem12  10329  hashbclem  14092  incexclem  15476  ramub1lem1  16655  ramub1lem2  16656  isstruct2  16778  setsdm  16799  mrieqvlemd  17255  mreexmrid  17269  islbs3  20332  lbsextlem4  20338  basdif0  22011  bwth  22469  locfincmp  22585  cldsubg  23170  nulmbl2  24605  volinun  24615  limcdif  24945  ellimc2  24946  limcmpt2  24953  dvreslem  24978  dvaddbr  25007  dvmulbr  25008  lhop  25085  plyeq0  25277  rlimcnp  26020  difeq  30766  ffsrn  30966  symgcom2  31255  esumpad2  31924  measunl  32084  subfacp1lem1  33041  cvmscld  33135  pibt2  35515  stoweidlem44  43475