Theorem undif1 4435

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4431). 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 4246	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4238	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4123	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4117	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4434	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2752	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4176	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4357	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2752	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2760	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293

This theorem is referenced by:  undif2  4436  undifr  4442  unidif0  5310  sofld  6148  fresaun  6713  ralxpmap  8846  enp1ilem  9199  difinf  9236  pwfilem  9243  infdif  10137  fin23lem11  10246  fin1a2lem13  10341  axcclem  10386  ttukeylem1  10438  ttukeylem7  10444  fpwwe2lem12  10571  hashbclem  14393  incexclem  15778  ramub1lem1  16973  ramub1lem2  16974  isstruct2  17095  setsdm  17116  mrieqvlemd  17570  mreexmrid  17584  islbs3  21097  lbsextlem4  21103  basdif0  22873  bwth  23330  locfincmp  23446  cldsubg  24031  nulmbl2  25470  volinun  25480  limcdif  25810  ellimc2  25811  limcmpt2  25818  dvreslem  25843  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  lhop  25954  plyeq0  26149  rlimcnp  26908  difeq  32497  ffsrn  32702  symgcom2  33056  esumpad2  34039  measunl  34199  subfacp1lem1  35159  cvmscld  35253  pibt2  37398  stoweidlem44  46035