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

Theorem dif0 3898
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 3896 . . 3
21difeq2i 3618 . 2
3 difdif 3629 . 2
42, 3eqtr3i 2488 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  \cdif 3472   c0 3784
This theorem is referenced by:  unvdif  3902  iinvdif  4402  dffv2  5946  2oconcl  7172  oe0m0  7189  oev2  7192  infdiffi  8095  cnfcom2lem  8166  cnfcom2lemOLD  8174  m1bits  14090  mreexdomd  15046  efgi0  16738  vrgpinv  16787  frgpuptinv  16789  frgpnabllem1  16877  gsumval3OLD  16908  gsumval3  16911  gsumcllem  16912  gsumcllemOLD  16913  dprddisj2  17087  dprddisj2OLD  17088  0cld  19539  indiscld  19592  mretopd  19593  hauscmplem  19906  ptbasfi  20082  cfinfil  20394  csdfil  20395  filufint  20421  bcth3  21770  rembl  21951  volsup  21966  disjdifprg  27436  prsiga  28131  sxbrsigalem3  28243  symdif0  29474  onint1  29914  dvmptfprodlem  31741  aacllem  33216  bj-disjdif  34511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785
  Copyright terms: Public domain W3C validator