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

Theorem dif0 4089
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 4087 . . 3 (𝐴𝐴) = ∅
21difeq2i 3864 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 3875 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2780 1 (𝐴 ∖ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1628  cdif 3708  c0 4054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ral 3051  df-rab 3055  df-v 3338  df-dif 3714  df-in 3718  df-ss 3725  df-nul 4055
This theorem is referenced by:  unvdif  4182  disjdif2  4187  iinvdif  4740  symdif0  4745  dffv2  6429  2oconcl  7748  oe0m0  7765  oev2  7768  infdiffi  8724  cnfcom2lem  8767  m1bits  15360  mreexdomd  16507  efgi0  18329  vrgpinv  18378  frgpuptinv  18380  frgpnabllem1  18472  gsumval3  18504  gsumcllem  18505  dprddisj2  18634  0cld  21040  indiscld  21093  mretopd  21094  hauscmplem  21407  cfinfil  21894  csdfil  21895  filufint  21921  bcth3  23324  rembl  23504  volsup  23520  disjdifprg  29691  prsiga  30499  sigapildsyslem  30529  sigapildsys  30530  sxbrsigalem3  30639  0elcarsg  30674  carsgclctunlem3  30687  onint1  32750  csbdif  33478  lindsdom  33712  ntrclscls00  38862  ntrclskb  38865  compne  39141  prsal  41037  saluni  41043  caragen0  41222  carageniuncllem1  41237  aacllem  43056
  Copyright terms: Public domain W3C validator