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

Theorem dif0 3865
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  |-  ( A 
\  (/) )  =  A

Proof of Theorem dif0
StepHypRef Expression
1 difid 3863 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3580 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3591 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2453 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    \ cdif 3433   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  unvdif  3869  disjdif2  3874  iinvdif  4368  symdif0  4373  dffv2  5951  2oconcl  7210  oe0m0  7227  oev2  7230  infdiffi  8165  cnfcom2lem  8208  m1bits  14402  mreexdomd  15543  efgi0  17358  vrgpinv  17407  frgpuptinv  17409  frgpnabllem1  17497  gsumval3  17529  gsumcllem  17530  dprddisj2  17660  0cld  20040  indiscld  20094  mretopd  20095  hauscmplem  20408  cfinfil  20895  csdfil  20896  filufint  20922  bcth3  22286  rembl  22481  volsup  22496  disjdifprg  28175  prsiga  28949  sigapildsyslem  28979  sigapildsys  28980  sxbrsigalem3  29090  0elcarsg  29135  carsgclctunlem3  29148  onint1  31102  csbdif  31677  prsal  37980  saluni  37986  caragen0  38106  carageniuncllem1  38121  aacllem  39814
  Copyright terms: Public domain W3C validator