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

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

Proof of Theorem undif1
StepHypRef Expression
1 undir 4241 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2 invdif 4233 . . 3 (𝐴 ∩ (V ∖ 𝐵)) = (𝐴𝐵)
32uneq1i 4124 . 2 ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴𝐵) ∪ 𝐵)
4 uncom 4118 . . . . 5 ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5 unvdif 4439 . . . . 5 (𝐵 ∪ (V ∖ 𝐵)) = V
64, 5eqtri 2765 . . . 4 ((V ∖ 𝐵) ∪ 𝐵) = V
76ineq2i 4174 . . 3 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴𝐵) ∩ V)
8 inv1 4359 . . 3 ((𝐴𝐵) ∩ V) = (𝐴𝐵)
97, 8eqtri 2765 . 2 ((𝐴𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴𝐵)
101, 3, 93eqtr3i 2773 1 ((𝐴𝐵) ∪ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Vcvv 3448  cdif 3912  cun 3913  cin 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288
This theorem is referenced by:  undif2  4441  unidif0  5320  sofld  6144  fresaun  6718  ralxpmap  8841  pwfilem  9128  enp1ilem  9229  difinf  9267  pwfilemOLD  9297  infdif  10152  fin23lem11  10260  fin1a2lem13  10355  axcclem  10400  ttukeylem1  10452  ttukeylem7  10458  fpwwe2lem12  10585  hashbclem  14356  incexclem  15728  ramub1lem1  16905  ramub1lem2  16906  isstruct2  17028  setsdm  17049  mrieqvlemd  17516  mreexmrid  17530  islbs3  20632  lbsextlem4  20638  basdif0  22319  bwth  22777  locfincmp  22893  cldsubg  23478  nulmbl2  24916  volinun  24926  limcdif  25256  ellimc2  25257  limcmpt2  25264  dvreslem  25289  dvaddbr  25318  dvmulbr  25319  lhop  25396  plyeq0  25588  rlimcnp  26331  difeq  31487  ffsrn  31688  symgcom2  31977  esumpad2  32695  measunl  32855  subfacp1lem1  33813  cvmscld  33907  pibt2  35917  stoweidlem44  44359
  Copyright terms: Public domain W3C validator