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

Theorem difun2 4000
 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 3839 . 2 ((𝐴𝐵) ∖ 𝐵) = ((𝐴𝐵) ∪ (𝐵𝐵))
2 difid 3902 . . 3 (𝐵𝐵) = ∅
32uneq2i 3726 . 2 ((𝐴𝐵) ∪ (𝐵𝐵)) = ((𝐴𝐵) ∪ ∅)
4 un0 3919 . 2 ((𝐴𝐵) ∪ ∅) = (𝐴𝐵)
51, 3, 43eqtri 2636 1 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∖ cdif 3537   ∪ cun 3538  ∅c0 3874 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875 This theorem is referenced by:  uneqdifeq  4009  uneqdifeqOLD  4010  difprsn1  4271  orddif  5737  domunsncan  7945  elfiun  8219  hartogslem1  8330  cantnfp1lem3  8460  cda1dif  8881  infcda1  8898  ssxr  9986  dfn2  11182  incexclem  14407  mreexmrid  16126  lbsextlem4  18982  ufprim  21523  volun  23120  i1f1  23263  itgioo  23388  itgsplitioo  23410  plyeq0lem  23770  jensen  24515  difeq  28739  fzdif2  28939  measun  29601  carsgclctunlem1  29706  carsggect  29707  elmrsubrn  30671  mrsubvrs  30673  finixpnum  32564  lindsenlbs  32574  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem16  32595  poimirlem18  32597  poimirlem19  32598  poimirlem21  32600  poimirlem23  32602  poimirlem27  32606  poimirlem30  32609  asindmre  32665  kelac2  36653  pwfi2f1o  36684  iccdifioo  38588  iccdifprioo  38589  hoiprodp1  39478
 Copyright terms: Public domain W3C validator