Theorem undif1 4439

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4435). 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 4250	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4242	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4127	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4121	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4438	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2752	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4180	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4361	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2752	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2760	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297

This theorem is referenced by:  undif2  4440  undifr  4446  unidif0  5315  sofld  6160  fresaun  6731  ralxpmap  8869  enp1ilem  9223  difinf  9260  pwfilem  9267  infdif  10161  fin23lem11  10270  fin1a2lem13  10365  axcclem  10410  ttukeylem1  10462  ttukeylem7  10468  fpwwe2lem12  10595  hashbclem  14417  incexclem  15802  ramub1lem1  16997  ramub1lem2  16998  isstruct2  17119  setsdm  17140  mrieqvlemd  17590  mreexmrid  17604  islbs3  21065  lbsextlem4  21071  basdif0  22840  bwth  23297  locfincmp  23413  cldsubg  23998  nulmbl2  25437  volinun  25447  limcdif  25777  ellimc2  25778  limcmpt2  25785  dvreslem  25810  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  lhop  25921  plyeq0  26116  rlimcnp  26875  difeq  32447  ffsrn  32652  symgcom2  33041  esumpad2  34046  measunl  34206  subfacp1lem1  35166  cvmscld  35260  pibt2  37405  stoweidlem44  46042