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

Theorem difun2 4439
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 4239 . 2 ((𝐴𝐵) ∖ 𝐵) = ((𝐴𝐵) ∪ (𝐵𝐵))
2 difid 4329 . . 3 (𝐵𝐵) = ∅
32uneq2i 4119 . 2 ((𝐴𝐵) ∪ (𝐵𝐵)) = ((𝐴𝐵) ∪ ∅)
4 un0 4349 . 2 ((𝐴𝐵) ∪ ∅) = (𝐴𝐵)
51, 3, 43eqtri 2768 1 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  cdif 3906  cun 3907  c0 4281
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-nul 4282
This theorem is referenced by:  undif5  4441  uneqdifeq  4449  difprsn1  4759  orddif  6412  domunsncan  9013  elfiun  9363  hartogslem1  9475  cantnfp1lem3  9613  dju1dif  10105  infdju1  10122  ssxr  11221  dfn2  12423  incexclem  15718  mreexmrid  17520  lbsextlem4  20618  ufprim  23256  volun  24905  i1f1  25050  itgioo  25176  itgsplitioo  25198  plyeq0lem  25567  jensen  26334  difeq  31343  fzdif2  31589  fzodif2  31590  pmtrcnel2  31836  measun  32701  carsgclctunlem1  32808  carsggect  32809  chtvalz  33133  elmrsubrn  34005  mrsubvrs  34007  pibt2  35877  finixpnum  36052  lindsadd  36060  lindsenlbs  36062  poimirlem2  36069  poimirlem4  36071  poimirlem6  36073  poimirlem7  36074  poimirlem8  36075  poimirlem11  36078  poimirlem12  36079  poimirlem13  36080  poimirlem14  36081  poimirlem16  36083  poimirlem18  36085  poimirlem19  36086  poimirlem21  36088  poimirlem23  36090  poimirlem27  36094  poimirlem30  36097  asindmre  36150  disjresundif  36689  kelac2  41368  pwfi2f1o  41399  iccdifioo  43723  iccdifprioo  43724  hoiprodp1  44799
  Copyright terms: Public domain W3C validator