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

Theorem dif0 4286
 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 4284 . . 3 (𝐴𝐴) = ∅
21difeq2i 4047 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 4058 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2823 1 (𝐴 ∖ ∅) = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∖ cdif 3878  ∅c0 4243 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244 This theorem is referenced by:  unvdif  4381  disjdif2  4386  iinvdif  4965  symdif0  4970  dffv2  6733  2oconcl  8111  oe0m0  8128  oev2  8131  infdiffi  9105  cnfcom2lem  9148  m1bits  15779  mreexdomd  16912  efgi0  18838  vrgpinv  18887  frgpuptinv  18889  frgpnabllem1  18986  gsumval3  19020  gsumcllem  19021  dprddisj2  19154  0cld  21643  indiscld  21696  mretopd  21697  hauscmplem  22011  cfinfil  22498  csdfil  22499  filufint  22525  bcth3  23935  rembl  24144  volsup  24160  disjdifprg  30338  tocycf  30809  tocyc01  30810  prsiga  31500  sigapildsyslem  31530  sigapildsys  31531  sxbrsigalem3  31640  0elcarsg  31675  carsgclctunlem3  31688  onint1  33907  csbdif  34739  lindsdom  35048  ntrclscls00  40764  ntrclskb  40767  compne  41140  prsal  42955  saluni  42961  caragen0  43140  carageniuncllem1  43155  aacllem  45324
 Copyright terms: Public domain W3C validator