Theorem nn0ex 12285

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.)

Assertion

Ref	Expression
nn0ex	⊢ ℕ0 ∈ V

Proof of Theorem nn0ex

Step	Hyp	Ref	Expression
1		df-n0 12280	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12025	. . 3 ⊢ ℕ ∈ V
3		snex 5363	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7628	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2833	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2104  Vcvv 3437   ∪ cun 3890  {csn 4565  0cc0 10917  ℕcn 12019  ℕ₀cn0 12279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-1cn 10975  ax-addcl 10977

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020  df-n0 12280

This theorem is referenced by:  nn0ennn  13745  nnenom  13746  fsuppmapnn0fiub0  13759  suppssfz  13760  fsuppmapnn0ub  13761  mptnn0fsupp  13763  mptnn0fsuppr  13765  wrdexg  14272  elovmptnn0wrd  14307  rtrclreclem1  14813  dfrtrclrec2  14814  rtrclreclem2  14815  rtrclreclem4  14817  expcnv  15621  geolim  15627  cvgrat  15640  mertenslem2  15642  bpolylem  15803  eftlub  15863  bitsfval  16175  bitsf  16179  sadfval  16204  smufval  16229  smupf  16230  1arith  16673  ramcl  16775  smndex1ibas  18584  smndex1gbas  18586  smndex1gid  18587  smndex1igid  18588  smndex1mnd  18594  smndex1id  18595  smndex1n0mnd  18596  smndex2dbas  18598  smndex2dnrinv  18599  smndex2hbas  18600  smndex2dlinvh  18601  odfval  19185  fsfnn0gsumfsffz  19629  gsummptnn0fz  19632  nn0srg  20713  psrbag  21165  evlsgsumadd  21346  evlsgsummul  21347  mhpfval  21374  mhpmulcl  21384  coe1fval  21421  fvcoe1  21423  coe1fval3  21424  coe1f2  21425  coe1sfi  21429  coe1fsupp  21430  00ply1bas  21456  ply1plusgfvi  21458  coe1z  21479  coe1add  21480  coe1addfv  21481  coe1mul2lem1  21483  coe1mul2lem2  21484  coe1mul2  21485  coe1tm  21489  coe1sclmul  21498  coe1sclmulfv  21499  coe1sclmul2  21500  ply1coefsupp  21511  ply1coe  21512  gsumsmonply1  21519  gsummoncoe1  21520  evls1gsumadd  21535  evls1gsummul  21536  evl1gsummul  21571  pmatcollpw1  21970  pmatcollpw2lem  21971  pmatcollpw2  21972  pmatcollpw3lem  21977  pm2mpcl  21991  idpm2idmp  21995  mply1topmatcllem  21997  mply1topmatcl  21999  mp2pm2mplem2  22001  mp2pm2mplem5  22004  mp2pm2mp  22005  pm2mpghmlem2  22006  pm2mpghm  22010  pm2mpmhmlem2  22013  monmat2matmon  22018  pm2mp  22019  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  cpmidpmatlem2  22065  cpmadumatpolylem1  22075  cpmadumatpolylem2  22076  chcoeffeqlem  22079  cayhamlem3  22081  cayhamlem4  22082  dyadmax  24807  cpnfval  25141  deg1ldg  25302  deg1leb  25305  deg1val  25306  deg1mul3  25325  deg1mul3le  25326  uc1pmon1p  25361  plyval  25399  elply2  25402  plyf  25404  elplyr  25407  plyeq0lem  25416  plyeq0  25417  plypf1  25418  plyaddlem1  25419  plyaddlem  25421  plymullem  25422  coeeulem  25430  coeeq  25433  dgrlem  25435  coeidlem  25443  coeaddlem  25455  coemulc  25461  coe0  25462  coesub  25463  dgradd2  25474  dgrcolem2  25480  plydivlem4  25501  plydiveu  25503  vieta1lem2  25516  taylfval  25563  pserval  25614  dvradcnv  25625  pserdvlem2  25632  abelthlem1  25635  abelthlem3  25637  abelthlem6  25640  logtayl  25860  leibpi  26137  sqff1o  26376  clwwlknonmpo  28498  eulerpartleme  32375  eulerpartlem1  32379  eulerpartlemt  32383  eulerpartgbij  32384  eulerpartlemr  32386  eulerpartlemmf  32387  eulerpartlemgvv  32388  eulerpartlemgs2  32392  eulerpartlemn  32393  fib0  32411  fib1  32412  fibp1  32413  lpadval  32701  knoppcnlem1  34718  knoppcnlem6  34723  poimirlem32  35853  heiborlem3  36015  sticksstones14  40158  sticksstones20  40164  eldiophb  40616  diophrw  40618  hbtlem1  40986  hbtlem7  40988  dgrsub2  40998  mpaaeu  41013  deg1mhm  41070  elrtrclrec  41327  brmptiunrelexpd  41329  brrtrclrec  41343  iunrelexp0  41348  iunrelexpmin2  41358  dfrtrcl3  41379  fvrtrcllb0d  41381  fvrtrcllb0da  41382  fvrtrcllb1d  41383  radcnvrat  41970  binomcxplemrat  42006  binomcxplemnotnn0  42012  expfac  43247  dvnprodlem1  43536  dvnprodlem2  43537  dvnprodlem3  43538  etransclem24  43848  etransclem25  43849  etransclem26  43850  etransclem28  43852  etransclem35  43859  etransclem37  43861  etransclem48  43872  fmtnoinf  45046  nn0mnd  45431  ply1mulgsum  45789  itcovalpclem1  46074  itcovalpclem2  46075  itcovalt2lem1  46079  itcovalt2lem2  46080  ackvalsuc1mpt  46082  ackval0  46084  ackendofnn0  46088  ackvalsucsucval  46092