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

Theorem dif0 3897
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 3895 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3619 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3630 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2498 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    \ cdif 3473   (/)c0 3785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786
This theorem is referenced by:  unvdif  3901  iinvdif  4397  dffv2  5940  2oconcl  7153  oe0m0  7170  oev2  7173  infdiffi  8074  cnfcom2lem  8145  cnfcom2lemOLD  8153  m1bits  13949  mreexdomd  14904  efgi0  16544  vrgpinv  16593  frgpuptinv  16595  frgpnabllem1  16680  gsumval3OLD  16711  gsumval3  16714  gsumcllem  16715  gsumcllemOLD  16716  dprddisj2  16889  dprddisj2OLD  16890  0cld  19333  indiscld  19386  mretopd  19387  hauscmplem  19700  ptbasfi  19845  cfinfil  20157  csdfil  20158  filufint  20184  bcth3  21533  rembl  21714  volsup  21729  disjdifprg  27137  prsiga  27799  sxbrsigalem3  27911  symdif0  29079  onint1  29519  bj-disjdif  33610
  Copyright terms: Public domain W3C validator