Theorem undif1 4481

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4477). 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 4292	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4284	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4173	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4167	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4480	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2762	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4224	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4403	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2762	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2770	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1536  Vcvv 3477   ∖ cdif 3959   ∪ cun 3960   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339

This theorem is referenced by:  undif2  4482  undifr  4488  unidif0  5365  sofld  6208  fresaun  6779  ralxpmap  8934  enp1ilem  9309  difinf  9346  pwfilem  9353  infdif  10245  fin23lem11  10354  fin1a2lem13  10449  axcclem  10494  ttukeylem1  10546  ttukeylem7  10552  fpwwe2lem12  10679  hashbclem  14487  incexclem  15868  ramub1lem1  17059  ramub1lem2  17060  isstruct2  17182  setsdm  17203  mrieqvlemd  17673  mreexmrid  17687  islbs3  21174  lbsextlem4  21180  basdif0  22975  bwth  23433  locfincmp  23549  cldsubg  24134  nulmbl2  25584  volinun  25594  limcdif  25925  ellimc2  25926  limcmpt2  25933  dvreslem  25958  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  lhop  26069  plyeq0  26264  rlimcnp  27022  difeq  32545  ffsrn  32746  symgcom2  33086  esumpad2  34036  measunl  34196  subfacp1lem1  35163  cvmscld  35257  pibt2  37399  stoweidlem44  45999