Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  undif1 Structured version   Visualization version   GIF version

Theorem undif1 4382
 Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4379). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
undif1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)

Proof of Theorem undif1
StepHypRef Expression
1 undir 4203 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2 invdif 4195 . . 3 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
32uneq1i 4086 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∪ 𝐵)
4 uncom 4080 . . . . 5 ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5 unvdif 4381 . . . . 5 (𝐵 ∪ (V ∖ 𝐵)) = V
64, 5eqtri 2821 . . . 4 ((V ∖ 𝐵) ∪ 𝐵) = V
76ineq2i 4136 . . 3 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴𝐵) ∩ V)
8 inv1 4302 . . 3 ((𝐴𝐵) ∩ V) = (𝐴𝐵)
97, 8eqtri 2821 . 2 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴𝐵)
101, 3, 93eqtr3i 2829 1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244 This theorem is referenced by:  undif2  4383  unidif0  5226  pwundifOLD  5423  sofld  6012  fresaun  6524  ralxpmap  8446  enp1ilem  8739  difinf  8775  pwfilem  8805  infdif  9623  fin23lem11  9731  fin1a2lem13  9826  axcclem  9871  ttukeylem1  9923  ttukeylem7  9929  fpwwe2lem12  10056  hashbclem  13809  incexclem  15186  ramub1lem1  16355  ramub1lem2  16356  isstruct2  16488  setsdm  16512  mrieqvlemd  16895  mreexmrid  16909  islbs3  19924  lbsextlem4  19930  basdif0  21568  bwth  22025  locfincmp  22141  cldsubg  22726  nulmbl2  24150  volinun  24160  limcdif  24489  ellimc2  24490  limcmpt2  24497  dvreslem  24522  dvaddbr  24551  dvmulbr  24552  lhop  24629  plyeq0  24818  rlimcnp  25561  difeq  30299  ffsrn  30501  symgcom2  30788  esumpad2  31440  measunl  31600  subfacp1lem1  32554  cvmscld  32648  pibt2  34853  stoweidlem44  42729
 Copyright terms: Public domain W3C validator