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

Theorem dif0 3903
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 3901 . . 3 (𝐴𝐴) = ∅
21difeq2i 3686 . 2 (𝐴 ∖ (𝐴𝐴)) = (𝐴 ∖ ∅)
3 difdif 3697 . 2 (𝐴 ∖ (𝐴𝐴)) = 𝐴
42, 3eqtr3i 2633 1 (𝐴 ∖ ∅) = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cdif 3536  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rab 2904  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874
This theorem is referenced by:  unvdif  3993  disjdif2  3998  iinvdif  4522  symdif0  4527  dffv2  6166  2oconcl  7447  oe0m0  7464  oev2  7467  infdiffi  8415  cnfcom2lem  8458  m1bits  14946  mreexdomd  16079  efgi0  17902  vrgpinv  17951  frgpuptinv  17953  frgpnabllem1  18045  gsumval3  18077  gsumcllem  18078  dprddisj2  18207  0cld  20594  indiscld  20647  mretopd  20648  hauscmplem  20961  cfinfil  21449  csdfil  21450  filufint  21476  bcth3  22853  rembl  23032  volsup  23048  disjdifprg  28576  prsiga  29327  sigapildsyslem  29357  sigapildsys  29358  sxbrsigalem3  29467  0elcarsg  29502  carsgclctunlem3  29515  onint1  31424  csbdif  32143  lindsdom  32369  ntrclscls00  37180  ntrclskb  37183  prsal  39011  saluni  39017  caragen0  39193  carageniuncllem1  39208  aacllem  42312
  Copyright terms: Public domain W3C validator