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

Theorem noel 3788
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
Assertion
Ref Expression
noel

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3625 . . 3
2 eldifn 3626 . . 3
31, 2pm2.65i 173 . 2
4 df-nul 3785 . . 3
54eleq2i 2535 . 2
63, 5mtbir 299 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  e.wcel 1818   cvv 3109  \cdif 3472   c0 3784
This theorem is referenced by:  n0i  3789  n0f  3793  rex0  3799  abvor0  3803  rab0  3806  un0  3810  in0  3811  0ss  3814  sbcel12  3823  sbcel2  3831  disj  3867  r19.2zb  3919  ral0  3934  rabsnifsb  4098  int0  4300  iun0  4386  0iun  4387  br0  4498  pwne0  4622  ord0eln0  4937  nlim0  4941  nsuceq0  4963  0xp  5085  csbxp  5086  dm0  5221  dm0rn0  5224  reldm0  5225  elimasni  5369  cnv0  5414  co02  5526  dffv3  5867  0fv  5904  mpt20  6367  bropopvvv  6880  tz7.44-2  7092  omordi  7234  omeulem1  7250  nnmordi  7299  omabs  7315  omsmolem  7321  0er  7365  omxpenlem  7638  en3lp  8054  cantnfle  8111  cantnfleOLD  8141  r1sdom  8213  r1pwss  8223  alephordi  8476  axdc3lem2  8852  zorn2lem7  8903  nlt1pi  9305  xrinfm0  11557  elixx3g  11571  elfz2  11708  fzm1  11787  om2uzlti  12061  hashf1lem2  12505  swrd0  12658  sum0  13543  fsumsplit  13562  sumsplit  13583  fsum2dlem  13585  prod0  13750  fprod2dlem  13784  sadc0  14104  sadcp1  14105  saddisjlem  14114  smu01lem  14135  smu01  14136  smu02  14137  prmreclem5  14438  vdwap0  14494  ram0  14540  0catg  15084  oduclatb  15774  0g0  15890  cntzrcl  16365  pmtrfrn  16483  psgnunilem5  16519  gexdvds  16604  gsumzsplit  16944  gsumzsplitOLD  16945  dprdcntz2  17086  00lss  17588  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  00ply1bas  18281  dsmmbas2  18768  dsmmfi  18769  maducoeval2  19142  madugsum  19145  0ntop  19414  haust1  19853  hauspwdom  20002  kqcldsat  20234  tsmssplit  20654  ustn0  20723  0met  20869  itg11  22098  itg0  22186  bddmulibl  22245  fsumharmonic  23341  ppiublem2  23478  lgsdir2lem3  23600  nbgra0edg  24432  uvtx01vtx  24492  clwwlknprop  24772  2wlkonot3v  24875  2spthonot3v  24876  rusgra0edg  24955  eupath2lem1  24977  helloworld  25173  isarchi  27726  measvuni  28185  ddemeas  28208  sibf0  28276  signstfvneq0  28529  opelco3  29208  wsuclem  29381  pw2f1ocnv  30979  areaquad  31184  iblempty  31764  stoweidlem34  31816  en3lpVD  33645  bj-projval  34554  bj-df-nul  34584  bj-nuliota  34586
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-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-v 3111  df-dif 3478  df-nul 3785
  Copyright terms: Public domain W3C validator