Theorem undif1 4499

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4495). 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 4306	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4298	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4187	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4181	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4498	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2768	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4238	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4421	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2768	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2776	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1537  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353

This theorem is referenced by:  undif2  4500  undifr  4506  unidif0  5378  sofld  6218  fresaun  6792  ralxpmap  8954  enp1ilem  9340  difinf  9377  pwfilem  9384  pwfilemOLD  9416  infdif  10277  fin23lem11  10386  fin1a2lem13  10481  axcclem  10526  ttukeylem1  10578  ttukeylem7  10584  fpwwe2lem12  10711  hashbclem  14501  incexclem  15884  ramub1lem1  17073  ramub1lem2  17074  isstruct2  17196  setsdm  17217  mrieqvlemd  17687  mreexmrid  17701  islbs3  21180  lbsextlem4  21186  basdif0  22981  bwth  23439  locfincmp  23555  cldsubg  24140  nulmbl2  25590  volinun  25600  limcdif  25931  ellimc2  25932  limcmpt2  25939  dvreslem  25964  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  lhop  26075  plyeq0  26270  rlimcnp  27026  difeq  32548  ffsrn  32743  symgcom2  33077  esumpad2  34020  measunl  34180  subfacp1lem1  35147  cvmscld  35241  pibt2  37383  stoweidlem44  45965