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

Theorem dif0 3537
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 3535 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3304 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3315 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2318 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632    \ cdif 3162   (/)c0 3468
This theorem is referenced by:  undifv  3541  dffv2  5608  2oconcl  6518  oe0m0  6535  oev2  6538  infdiffi  7374  cnfcom2lem  7420  m1bits  12647  mreexdomd  13567  efgi0  15045  vrgpinv  15094  frgpuptinv  15096  frgpnabllem1  15177  gsumval3  15207  gsumcllem  15209  dprddisj2  15290  0cld  16791  indiscld  16844  mretopd  16845  hauscmplem  17149  ptbasfi  17292  cfinfil  17604  csdfil  17605  filufint  17631  bcth3  18769  rembl  18914  volsup  18929  disjdifprg  23367  prsiga  23507  symdif0  24439  onint1  24960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rab 2565  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator