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

Theorem difun2 4192
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 4023 . 2 ((𝐴𝐵) ∖ 𝐵) = ((𝐴𝐵) ∪ (𝐵𝐵))
2 difid 4091 . . 3 (𝐵𝐵) = ∅
32uneq2i 3907 . 2 ((𝐴𝐵) ∪ (𝐵𝐵)) = ((𝐴𝐵) ∪ ∅)
4 un0 4110 . 2 ((𝐴𝐵) ∪ ∅) = (𝐴𝐵)
51, 3, 43eqtri 2786 1 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  cdif 3712  cun 3713  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059
This theorem is referenced by:  uneqdifeq  4201  uneqdifeqOLD  4202  difprsn1  4475  orddif  5981  domunsncan  8225  elfiun  8501  hartogslem1  8612  cantnfp1lem3  8750  cda1dif  9190  infcda1  9207  ssxr  10299  dfn2  11497  incexclem  14767  mreexmrid  16505  lbsextlem4  19363  ufprim  21914  volun  23513  i1f1  23656  itgioo  23781  itgsplitioo  23803  plyeq0lem  24165  jensen  24914  difeq  29662  fzdif2  29860  fzodif2  29861  measun  30583  carsgclctunlem1  30688  carsggect  30689  chtvalz  31016  elmrsubrn  31724  mrsubvrs  31726  finixpnum  33707  lindsenlbs  33717  poimirlem2  33724  poimirlem4  33726  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem11  33733  poimirlem12  33734  poimirlem13  33735  poimirlem14  33736  poimirlem16  33738  poimirlem18  33740  poimirlem19  33741  poimirlem21  33743  poimirlem23  33745  poimirlem27  33749  poimirlem30  33752  asindmre  33808  kelac2  38137  pwfi2f1o  38168  iccdifioo  40244  iccdifprioo  40245  hoiprodp1  41308
  Copyright terms: Public domain W3C validator