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

Theorem dif0 4329
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 4327 . . 3 (𝐴𝐴) = ∅
21difeq2i 4093 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 4104 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2843 1 (𝐴 ∖ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  cdif 3930  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289
This theorem is referenced by:  unvdif  4419  disjdif2  4424  iinvdif  4993  symdif0  4998  dffv2  6749  2oconcl  8117  oe0m0  8134  oev2  8137  infdiffi  9109  cnfcom2lem  9152  m1bits  15777  mreexdomd  16908  efgi0  18775  vrgpinv  18824  frgpuptinv  18826  frgpnabllem1  18922  gsumval3  18956  gsumcllem  18957  dprddisj2  19090  0cld  21574  indiscld  21627  mretopd  21628  hauscmplem  21942  cfinfil  22429  csdfil  22430  filufint  22456  bcth3  23861  rembl  24068  volsup  24084  disjdifprg  30253  tocycf  30686  tocyc01  30687  prsiga  31289  sigapildsyslem  31319  sigapildsys  31320  sxbrsigalem3  31429  0elcarsg  31464  carsgclctunlem3  31477  onint1  33694  csbdif  34488  lindsdom  34767  ntrclscls00  40294  ntrclskb  40297  compne  40650  prsal  42480  saluni  42486  caragen0  42665  carageniuncllem1  42680  aacllem  44830
  Copyright terms: Public domain W3C validator