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

Theorem noel 3618
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

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3455 . . 3
2 eldifn 3456 . . 3
31, 2pm2.65i 168 . 2
4 df-nul 3615 . . 3
54eleq2i 2486 . 2
63, 5mtbir 293 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  e.wcel 1749   cvv 2951  \cdif 3302   c0 3614
This theorem is referenced by:  n0i  3619  n0f  3622  rex0  3628  abvor0  3632  rab0  3635  un0  3639  in0  3640  0ss  3643  sbcel12  3652  sbcel2  3660  disj  3696  r19.2zb  3747  ral0  3761  int0  4117  iun0  4201  0iun  4202  br0  4313  sbcbr123  4318  pwne0  4434  ord0eln0  4744  nlim0  4748  nsuceq0  4770  0xp  4888  csbxp  4889  dm0  5024  dm0rn0  5027  reldm0  5028  elimasni  5168  cnv0  5212  co02  5323  dffv3  5657  0fv  5693  mpt20  6126  bropopvvv  6622  tz7.44-2  6822  0we1  6907  omordi  6966  omeulem1  6982  nnmordi  7031  omabs  7047  omsmolem  7053  0er  7097  omxpenlem  7371  en3lp  7769  cantnfle  7826  cantnfleOLD  7856  r1sdom  7928  r1pwss  7938  alephordi  8191  axdc3lem2  8567  zorn2lem7  8618  brdom3  8642  canthwe  8764  nlt1pi  9021  xrinfm0  11244  elixx3g  11258  elfz2  11388  om2uzlti  11714  hashf1lem2  12150  swrd0  12268  sum0  13139  fsumsplit  13157  sumsplit  13176  fsum2dlem  13178  sadc0  13590  sadcp1  13591  saddisjlem  13600  smu01lem  13621  smu01  13622  smu02  13623  prmreclem5  13921  vdwap0  13977  ram0  14023  0catg  14565  oduclatb  15254  0g0  15374  cntzrcl  15782  pmtrfrn  15901  psgnunilem5  15937  gexdvds  16020  gsumzsplit  16333  dprdcntz2  16405  00lss  16832  mplcoe1  17351  mplcoe2  17353  mplrcl  17373  strov2rcl  17456  00ply1bas  17459  dsmmbas2  17870  dsmmfi  17871  maducoeval2  18150  madugsum  18153  0ntop  18222  haust1  18660  hauspwdom  18809  kqcldsat  19010  tsmssplit  19426  ustn0  19495  0met  19641  itg11  20869  itg0  20957  bddmulibl  21016  fsumharmonic  22146  ppiublem2  22283  lgsdir2lem3  22405  nbgra0edg  23022  uvtx01vtx  23079  eupath2lem1  23277  helloworld  23337  isarchi  25878  measvuni  26337  ddemeas  26361  sibf0  26423  signstfvneq0  26676  prod0  27158  fprod2dlem  27193  opelco3  27291  wsuclem  27464  pw2f1ocnv  29059  areaquad  29265  stoweidlem34  29503  2wlkonot3v  30068  2spthonot3v  30069  clwwlknprop  30109  rusgra0edg  30247  rabsnif  30390  gsumpr  30423  gsumXzsplit  30481  en3lpVD  31159  bj-projval  31936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-v 2953  df-dif 3308  df-nul 3615
  Copyright terms: Public domain W3C validator