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

Theorem nn0ex 11895
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 11890 . 2 0 = (ℕ ∪ {0})
2 nnex 11635 . . 3 ℕ ∈ V
3 snex 5300 . . 3 {0} ∈ V
42, 3unex 7453 . 2 (ℕ ∪ {0}) ∈ V
51, 4eqeltri 2889 1 0 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  Vcvv 3444  cun 3882  {csn 4528  0cc0 10530  cn 11629  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-1cn 10588  ax-addcl 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-n0 11890
This theorem is referenced by:  nn0ennn  13346  nnenom  13347  fsuppmapnn0fiub0  13360  suppssfz  13361  fsuppmapnn0ub  13362  mptnn0fsupp  13364  mptnn0fsuppr  13366  wrdexg  13871  elovmptnn0wrd  13906  dfrtrclrec2  14411  rtrclreclem1  14412  rtrclreclem2  14413  rtrclreclem4  14415  expcnv  15214  geolim  15221  cvgrat  15234  mertenslem2  15236  bpolylem  15397  eftlub  15457  bitsfval  15765  bitsf  15769  sadfval  15794  smufval  15819  smupf  15820  1arith  16256  ramcl  16358  smndex1ibas  18060  smndex1gbas  18062  smndex1gid  18063  smndex1igid  18064  smndex1mnd  18070  smndex1id  18071  smndex1n0mnd  18072  smndex2dbas  18074  smndex2dnrinv  18075  smndex2hbas  18076  smndex2dlinvh  18077  odfval  18655  fsfnn0gsumfsffz  19099  gsummptnn0fz  19102  nn0srg  20164  psrbag  20605  evlsgsumadd  20766  evlsgsummul  20767  mhpfval  20794  coe1fval  20837  fvcoe1  20839  coe1fval3  20840  coe1f2  20841  coe1sfi  20845  coe1fsupp  20846  00ply1bas  20872  ply1plusgfvi  20874  coe1z  20895  coe1add  20896  coe1addfv  20897  coe1mul2lem1  20899  coe1mul2lem2  20900  coe1mul2  20901  coe1tm  20905  coe1sclmul  20914  coe1sclmulfv  20915  coe1sclmul2  20916  ply1coefsupp  20927  ply1coe  20928  gsumsmonply1  20935  gsummoncoe1  20936  evls1gsumadd  20951  evls1gsummul  20952  evl1gsummul  20987  pmatcollpw1  21384  pmatcollpw2lem  21385  pmatcollpw2  21386  pmatcollpw3lem  21391  pm2mpcl  21405  idpm2idmp  21409  mply1topmatcllem  21411  mply1topmatcl  21413  mp2pm2mplem2  21415  mp2pm2mplem5  21418  mp2pm2mp  21419  pm2mpghmlem2  21420  pm2mpghm  21424  pm2mpmhmlem2  21427  monmat2matmon  21432  pm2mp  21433  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmidpmatlem2  21479  cpmadumatpolylem1  21489  cpmadumatpolylem2  21490  chcoeffeqlem  21493  cayhamlem3  21495  cayhamlem4  21496  dyadmax  24205  cpnfval  24538  deg1ldg  24696  deg1leb  24699  deg1val  24700  deg1mul3  24719  deg1mul3le  24720  uc1pmon1p  24755  plyval  24793  elply2  24796  plyf  24798  elplyr  24801  plyeq0lem  24810  plyeq0  24811  plypf1  24812  plyaddlem1  24813  plyaddlem  24815  plymullem  24816  coeeulem  24824  coeeq  24827  dgrlem  24829  coeidlem  24837  coeaddlem  24849  coemulc  24855  coe0  24856  coesub  24857  dgradd2  24868  dgrcolem2  24874  plydivlem4  24895  plydiveu  24897  vieta1lem2  24910  taylfval  24957  pserval  25008  dvradcnv  25019  pserdvlem2  25026  abelthlem1  25029  abelthlem3  25031  abelthlem6  25034  logtayl  25254  leibpi  25531  sqff1o  25770  clwwlknonmpo  27877  eulerpartleme  31729  eulerpartlem1  31733  eulerpartlemt  31737  eulerpartgbij  31738  eulerpartlemr  31740  eulerpartlemmf  31741  eulerpartlemgvv  31742  eulerpartlemgs2  31746  eulerpartlemn  31747  fib0  31765  fib1  31766  fibp1  31767  lpadval  32055  knoppcnlem1  33940  knoppcnlem6  33945  poimirlem32  35082  heiborlem3  35244  eldiophb  39685  diophrw  39687  hbtlem1  40054  hbtlem7  40056  dgrsub2  40066  mpaaeu  40081  deg1mhm  40138  elrtrclrec  40369  brmptiunrelexpd  40371  brrtrclrec  40385  iunrelexp0  40390  iunrelexpmin2  40400  dfrtrcl3  40421  fvrtrcllb0d  40423  fvrtrcllb0da  40424  fvrtrcllb1d  40425  radcnvrat  41005  binomcxplemrat  41041  binomcxplemnotnn0  41047  expfac  42286  dvnprodlem1  42575  dvnprodlem2  42576  dvnprodlem3  42577  etransclem24  42887  etransclem25  42888  etransclem26  42889  etransclem28  42891  etransclem35  42898  etransclem37  42900  etransclem48  42911  fmtnoinf  44040  nn0mnd  44426  ply1mulgsum  44785  itcovalpclem1  45071  itcovalpclem2  45072  itcovalt2lem1  45076  itcovalt2lem2  45077  ackvalsuc1mpt  45079  ackval0  45081  ackendofnn0  45085  ackvalsucsucval  45089
  Copyright terms: Public domain W3C validator