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

Theorem difun2 4190
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 4021 . 2 ((𝐴𝐵) ∖ 𝐵) = ((𝐴𝐵) ∪ (𝐵𝐵))
2 difid 4089 . . 3 (𝐵𝐵) = ∅
32uneq2i 3905 . 2 ((𝐴𝐵) ∪ (𝐵𝐵)) = ((𝐴𝐵) ∪ ∅)
4 un0 4108 . 2 ((𝐴𝐵) ∪ ∅) = (𝐴𝐵)
51, 3, 43eqtri 2784 1 ((𝐴𝐵) ∖ 𝐵) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  cdif 3710  cun 3711  c0 4056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057
This theorem is referenced by:  uneqdifeq  4199  uneqdifeqOLD  4200  difprsn1  4473  orddif  5979  domunsncan  8223  elfiun  8499  hartogslem1  8610  cantnfp1lem3  8748  cda1dif  9188  infcda1  9205  ssxr  10297  dfn2  11495  incexclem  14765  mreexmrid  16503  lbsextlem4  19361  ufprim  21912  volun  23511  i1f1  23654  itgioo  23779  itgsplitioo  23801  plyeq0lem  24163  jensen  24912  difeq  29660  fzdif2  29858  fzodif2  29859  measun  30581  carsgclctunlem1  30686  carsggect  30687  chtvalz  31014  elmrsubrn  31722  mrsubvrs  31724  finixpnum  33705  lindsenlbs  33715  poimirlem2  33722  poimirlem4  33724  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem14  33734  poimirlem16  33736  poimirlem18  33738  poimirlem19  33739  poimirlem21  33741  poimirlem23  33743  poimirlem27  33747  poimirlem30  33750  asindmre  33806  kelac2  38135  pwfi2f1o  38166  iccdifioo  40242  iccdifprioo  40243  hoiprodp1  41306
  Copyright terms: Public domain W3C validator