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

Theorem dif0 3466
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 3464 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3233 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3244 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2278 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3091   (/)c0 3397
This theorem is referenced by:  undifv  3470  dffv2  5491  2oconcl  6435  oe0m0  6452  oev2  6455  infdiffi  7291  cnfcom2lem  7337  m1bits  12558  mreexdomd  13478  efgi0  14956  vrgpinv  15005  frgpuptinv  15007  frgpnabllem1  15088  gsumval3  15118  gsumcllem  15120  dprddisj2  15201  0cld  16702  indiscld  16755  mretopd  16756  hauscmplem  17060  ptbasfi  17203  cfinfil  17515  csdfil  17516  filufint  17542  bcth3  18680  rembl  18825  volsup  18840  symdif0  23709  onint1  24228
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rab 2523  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398
  Copyright terms: Public domain W3C validator