MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0ex Structured version   Visualization version   GIF version

Theorem nn0ex 11148
Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)
Assertion
Ref Expression
nn0ex 0 ∈ V

Proof of Theorem nn0ex
StepHypRef Expression
1 df-n0 11143 . 2 0 = (ℕ ∪ {0})
2 nnex 10876 . . 3 ℕ ∈ V
3 snex 4830 . . 3 {0} ∈ V
42, 3unex 6832 . 2 (ℕ ∪ {0}) ∈ V
51, 4eqeltri 2683 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3172  cun 3537  {csn 4124  0cc0 9793  cn 10870  0cn0 11142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-i2m1 9861  ax-1ne0 9862  ax-rrecex 9865  ax-cnre 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-nn 10871  df-n0 11143
This theorem is referenced by:  nn0ennn  12598  nnenom  12599  fsuppmapnn0fiub0  12613  suppssfz  12614  fsuppmapnn0ub  12615  mptnn0fsupp  12617  mptnn0fsuppr  12619  elovmptnn0wrd  13152  dfrtrclrec2  13594  rtrclreclem1  13595  rtrclreclem2  13596  rtrclreclem4  13598  expcnv  14384  geolim  14389  cvgrat  14403  mertenslem2  14405  bpolylem  14567  eftlub  14627  bitsfval  14932  bitsf  14936  sadfval  14961  smufval  14986  smupf  14987  1arith  15418  ramcl  15520  fsfnn0gsumfsffz  18151  gsummptnn0fz  18154  psrbag  19134  coe1fval  19345  fvcoe1  19347  coe1fval3  19348  coe1f2  19349  coe1sfi  19353  coe1fsupp  19354  00ply1bas  19380  ply1plusgfvi  19382  coe1z  19403  coe1add  19404  coe1addfv  19405  coe1mul2lem1  19407  coe1mul2lem2  19408  coe1mul2  19409  coe1tm  19413  coe1sclmul  19422  coe1sclmulfv  19423  coe1sclmul2  19424  ply1coefsupp  19435  ply1coe  19436  gsumsmonply1  19443  gsummoncoe1  19444  evls1gsumadd  19459  evls1gsummul  19460  evl1gsummul  19494  nn0srg  19584  pmatcollpw1  20348  pmatcollpw2lem  20349  pmatcollpw2  20350  pmatcollpw3lem  20355  pm2mpcl  20369  idpm2idmp  20373  mply1topmatcllem  20375  mply1topmatcl  20377  mp2pm2mplem2  20379  mp2pm2mplem5  20382  mp2pm2mp  20383  pm2mpghmlem2  20384  pm2mpghm  20388  pm2mpmhmlem2  20391  monmat2matmon  20396  pm2mp  20397  chfacfscmulgsum  20432  chfacfpmmulgsum  20436  cpmidpmatlem2  20443  cpmadumatpolylem1  20453  cpmadumatpolylem2  20454  chcoeffeqlem  20457  cayhamlem3  20459  cayhamlem4  20460  dyadmax  23117  cpnfval  23446  deg1ldg  23601  deg1leb  23604  deg1val  23605  deg1mul3  23624  deg1mul3le  23625  uc1pmon1p  23660  plyval  23698  elply2  23701  plyf  23703  elplyr  23706  plyeq0lem  23715  plyeq0  23716  plypf1  23717  plyaddlem1  23718  plyaddlem  23720  plymullem  23721  coeeulem  23729  coeeq  23732  dgrlem  23734  coeidlem  23742  coeaddlem  23754  coemulc  23760  coe0  23761  coesub  23762  dgradd2  23773  dgrcolem2  23779  plydivlem4  23800  plydiveu  23802  vieta1lem2  23815  taylfval  23862  pserval  23913  dvradcnv  23924  pserdvlem2  23931  abelthlem1  23934  abelthlem3  23936  abelthlem6  23939  logtayl  24151  leibpi  24414  sqff1o  24653  wwlkn  26004  clwwlkn  26089  clwwlknprop  26094  iseupa  26286  eulerpartleme  29586  eulerpartlem1  29590  eulerpartlemt  29594  eulerpartgbij  29595  eulerpartlemr  29597  eulerpartlemmf  29598  eulerpartlemgvv  29599  eulerpartlemgs2  29603  eulerpartlemn  29604  fib0  29622  fib1  29623  fibp1  29624  knoppcnlem1  31487  knoppcnlem6  31492  poimirlem32  32435  heiborlem3  32606  eldiophb  36162  diophrw  36164  hbtlem1  36536  hbtlem7  36538  dgrsub2  36548  mpaaeu  36563  deg1mhm  36628  elrtrclrec  36816  brmptiunrelexpd  36818  brrtrclrec  36832  iunrelexp0  36837  iunrelexpmin2  36847  dfrtrcl3  36868  fvrtrcllb0d  36870  fvrtrcllb0da  36871  fvrtrcllb1d  36872  radcnvrat  37359  binomcxplemrat  37395  binomcxplemnotnn0  37401  expfac  38548  dvnprodlem1  38660  dvnprodlem2  38661  dvnprodlem3  38662  etransclem24  38975  etransclem25  38976  etransclem26  38977  etransclem28  38979  etransclem35  38986  etransclem37  38988  etransclem48  38999  fmtnoinf  39811  ply1mulgsum  41994
  Copyright terms: Public domain W3C validator