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

Theorem difun2 4387
 Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
difun2 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)

Proof of Theorem difun2
StepHypRef Expression
1 difundir 4207 . 2 ((𝐴𝐵) ∖ 𝐵) = ((𝐴𝐵) ∪ (𝐵𝐵))
2 difid 4284 . . 3 (𝐵𝐵) = ∅
32uneq2i 4087 . 2 ((𝐴𝐵) ∪ (𝐵𝐵)) = ((𝐴𝐵) ∪ ∅)
4 un0 4298 . 2 ((𝐴𝐵) ∪ ∅) = (𝐴𝐵)
51, 3, 43eqtri 2825 1 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∖ cdif 3878   ∪ cun 3879  ∅c0 4243 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:  uneqdifeq  4396  difprsn1  4693  orddif  6252  domunsncan  8602  elfiun  8880  hartogslem1  8992  cantnfp1lem3  9129  dju1dif  9585  infdju1  9602  ssxr  10701  dfn2  11900  incexclem  15185  mreexmrid  16908  lbsextlem4  19929  ufprim  22521  volun  24156  i1f1  24301  itgioo  24426  itgsplitioo  24448  plyeq0lem  24814  jensen  25581  difeq  30296  undif5  30298  fzdif2  30547  fzodif2  30548  pmtrcnel2  30791  measun  31592  carsgclctunlem1  31697  carsggect  31698  chtvalz  32022  elmrsubrn  32892  mrsubvrs  32894  pibt2  34850  finixpnum  35058  lindsadd  35066  lindsenlbs  35068  poimirlem2  35075  poimirlem4  35077  poimirlem6  35079  poimirlem7  35080  poimirlem8  35081  poimirlem11  35084  poimirlem12  35085  poimirlem13  35086  poimirlem14  35087  poimirlem16  35089  poimirlem18  35091  poimirlem19  35092  poimirlem21  35094  poimirlem23  35096  poimirlem27  35100  poimirlem30  35103  asindmre  35156  kelac2  40024  pwfi2f1o  40055  iccdifioo  42167  iccdifprioo  42168  hoiprodp1  43242
 Copyright terms: Public domain W3C validator