Theorem undif1 4426

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4422). 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 4237	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4229	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4114	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4108	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4425	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2757	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4167	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4348	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2757	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2765	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1541  Vcvv 3438   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284

This theorem is referenced by:  undif2  4427  undifr  4433  unidif0  5303  sofld  6143  fresaun  6703  ralxpmap  8832  enp1ilem  9176  difinf  9209  pwfilem  9216  infdif  10116  fin23lem11  10225  fin1a2lem13  10320  axcclem  10365  ttukeylem1  10417  ttukeylem7  10423  fpwwe2lem12  10551  hashbclem  14373  incexclem  15757  ramub1lem1  16952  ramub1lem2  16953  isstruct2  17074  setsdm  17095  mrieqvlemd  17550  mreexmrid  17564  islbs3  21108  lbsextlem4  21114  basdif0  22895  bwth  23352  locfincmp  23468  cldsubg  24053  nulmbl2  25491  volinun  25501  limcdif  25831  ellimc2  25832  limcmpt2  25839  dvreslem  25864  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  lhop  25975  plyeq0  26170  rlimcnp  26929  difeq  32542  ffsrn  32756  symgcom2  33115  esumpad2  34162  measunl  34322  subfacp1lem1  35322  cvmscld  35416  pibt2  37561  stoweidlem44  46230