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

Theorem dif0 3904
 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 3902 . . 3 (𝐴𝐴) = ∅
21difeq2i 3687 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 3698 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2634 1 (𝐴 ∖ ∅) = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∖ cdif 3537  ∅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-in 3547  df-ss 3554  df-nul 3875 This theorem is referenced by:  unvdif  3994  disjdif2  3999  iinvdif  4528  symdif0  4533  dffv2  6181  2oconcl  7470  oe0m0  7487  oev2  7490  infdiffi  8438  cnfcom2lem  8481  m1bits  15000  mreexdomd  16133  efgi0  17956  vrgpinv  18005  frgpuptinv  18007  frgpnabllem1  18099  gsumval3  18131  gsumcllem  18132  dprddisj2  18261  0cld  20652  indiscld  20705  mretopd  20706  hauscmplem  21019  cfinfil  21507  csdfil  21508  filufint  21534  bcth3  22936  rembl  23115  volsup  23131  disjdifprg  28770  prsiga  29521  sigapildsyslem  29551  sigapildsys  29552  sxbrsigalem3  29661  0elcarsg  29696  carsgclctunlem3  29709  onint1  31618  csbdif  32347  lindsdom  32573  ntrclscls00  37384  ntrclskb  37387  prsal  39214  saluni  39220  caragen0  39396  carageniuncllem1  39411  aacllem  42356
 Copyright terms: Public domain W3C validator