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

Theorem noel 3461
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
Assertion
Ref Expression
noel  |-  -.  A  e.  (/)

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3300 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3301 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 165 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3458 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2349 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 290 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1686   _Vcvv 2790    \ cdif 3151   (/)c0 3457
This theorem is referenced by:  n0i  3462  n0f  3465  rex0  3470  abvor0  3474  rab0  3477  un0  3481  in0  3482  0ss  3485  disj  3497  r19.2zb  3546  ral0  3560  int0  3878  iun0  3960  0iun  3961  ord0eln0  4448  nlim0  4452  nsuceq0  4474  xp0r  4770  dm0  4894  dm0rn0  4897  reldm0  4898  elimasni  5042  cnv0  5086  co02  5188  dffv3  5523  fv01  5561  mpt20  6201  tz7.44-2  6422  0we1  6507  omordi  6566  omeulem1  6582  nnmordi  6631  omabs  6647  omsmolem  6653  0er  6697  omxpenlem  6965  cantnfle  7374  en3lp  7420  r1sdom  7448  r1pwss  7458  alephordi  7703  axdc3lem2  8079  zorn2lem7  8131  brdom3  8155  canthwe  8275  nlt1pi  8532  xrinfm0  10657  elixx3g  10671  elfz2  10791  om2uzlti  11015  hashf1lem2  11396  sum0  12196  fsumsplit  12214  sumsplit  12233  fsum2dlem  12235  sadc0  12647  sadcp1  12648  saddisjlem  12657  smu01lem  12678  smu01  12679  smu02  12680  prmreclem5  12969  vdwap0  13025  ram0  13071  0catg  13591  oduclatb  14250  0g0  14388  cntzrcl  14805  gexdvds  14897  gsumzsplit  15208  dprdcntz2  15275  00lss  15701  mplcoe1  16211  mplcoe2  16213  mplrcl  16233  strov2rcl  16317  00ply1bas  16320  0ntop  16653  haust1  17082  hauspwdom  17229  kqcldsat  17426  tsmssplit  17836  0met  17932  itg11  19048  itg0  19136  bddmulibl  19195  fsumharmonic  20307  ppiublem2  20444  lgsdir2lem3  20566  helloworld  20840  measvuni  23544  eupath2lem1  23903  funpartfv  24485  elioo1t3  25513  0ded  25768  0catOLD  25769  pw2f1ocnv  27141  dsmmbas2  27214  dsmmfi  27215  pmtrfrn  27411  psgnunilem5  27428  stoweidlem34  27794  nbgra0edg  28158  uvtx01vtx  28175  en3lpVD  28694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-nul 3458
  Copyright terms: Public domain W3C validator