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

Theorem dif0 4333
Description: The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
dif0 (𝐴 ∖ ∅) = 𝐴

Proof of Theorem dif0
StepHypRef Expression
1 difid 4331 . . 3 (𝐴𝐴) = ∅
21difeq2i 4080 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 4091 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2763 1 (𝐴 ∖ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3908  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-nul 4284
This theorem is referenced by:  unvdif  4435  disjdif2  4440  csbdif  4486  iinvdif  5041  symdif0  5046  dffv2  6937  2oconcl  8450  oe0m0  8467  oev2  8470  infdiffi  9599  cnfcom2lem  9642  brttrcl2  9655  ttrcltr  9657  rnttrcl  9663  m1bits  16325  mreexdomd  17534  efgi0  19507  vrgpinv  19556  frgpuptinv  19558  frgpnabllem1  19656  gsumval3  19689  gsumcllem  19690  dprddisj2  19823  0cld  22405  indiscld  22458  mretopd  22459  hauscmplem  22773  cfinfil  23260  csdfil  23261  filufint  23287  bcth3  24711  rembl  24920  volsup  24936  new0  27226  disjdifprg  31539  tocycf  32015  tocyc01  32016  prsiga  32787  sigapildsyslem  32817  sigapildsys  32818  sxbrsigalem3  32929  0elcarsg  32964  carsgclctunlem3  32977  onint1  34967  lindsdom  36118  oe0rif  41663  ntrclscls00  42426  ntrclskb  42429  compne  42809  prsal  44645  saluni  44652  caragen0  44833  carageniuncllem1  44848  iscnrm3rlem4  47062  aacllem  47334
  Copyright terms: Public domain W3C validator