Theorem nn0ex 12530

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 12525	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12270	. . 3 ⊢ ℕ ∈ V
3		snex 5437	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7754	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2822	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3462   ∪ cun 3945  {csn 4633  0cc0 11158  ℕcn 12264  ℕ₀cn0 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-1cn 11216  ax-addcl 11218

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-nn 12265  df-n0 12525

This theorem is referenced by:  nn0ennn  13999  nnenom  14000  fsuppmapnn0fiub0  14013  suppssfz  14014  fsuppmapnn0ub  14015  mptnn0fsupp  14017  mptnn0fsuppr  14019  wrdexg  14532  elovmptnn0wrd  14567  rtrclreclem1  15062  dfrtrclrec2  15063  rtrclreclem2  15064  rtrclreclem4  15066  expcnv  15868  geolim  15874  cvgrat  15887  mertenslem2  15889  bpolylem  16050  eftlub  16111  bitsfval  16423  bitsf  16427  sadfval  16452  smufval  16477  smupf  16478  1arith  16929  ramcl  17031  smndex1ibas  18890  smndex1gbas  18892  smndex1gid  18893  smndex1igid  18894  smndex1mnd  18900  smndex1id  18901  smndex1n0mnd  18902  smndex2dbas  18904  smndex2dnrinv  18905  smndex2hbas  18906  smndex2dlinvh  18907  odfval  19530  fsfnn0gsumfsffz  19981  gsummptnn0fz  19984  nn0srg  21434  psrbag  21914  evlsgsumadd  22106  evlsgsummul  22107  mhpfval  22133  mhpmulcl  22143  coe1fval  22195  fvcoe1  22197  coe1fval3  22198  coe1f2  22199  coe1sfi  22203  coe1fsupp  22204  00ply1bas  22229  ply1plusgfvi  22231  coe1z  22254  coe1add  22255  coe1addfv  22256  coe1mul2lem1  22258  coe1mul2lem2  22259  coe1mul2  22260  coe1tm  22264  coe1sclmul  22273  coe1sclmulfv  22274  coe1sclmul2  22275  ply1coefsupp  22288  ply1coe  22289  gsumsmonply1  22298  gsummoncoe1  22299  evls1gsumadd  22315  evls1gsummul  22316  evl1gsummul  22351  evls1fpws  22360  pmatcollpw1  22769  pmatcollpw2lem  22770  pmatcollpw2  22771  pmatcollpw3lem  22776  pm2mpcl  22790  idpm2idmp  22794  mply1topmatcllem  22796  mply1topmatcl  22798  mp2pm2mplem2  22800  mp2pm2mplem5  22803  mp2pm2mp  22804  pm2mpghmlem2  22805  pm2mpghm  22809  pm2mpmhmlem2  22812  monmat2matmon  22817  pm2mp  22818  chfacfscmulgsum  22853  chfacfpmmulgsum  22857  cpmidpmatlem2  22864  cpmadumatpolylem1  22874  cpmadumatpolylem2  22875  chcoeffeqlem  22878  cayhamlem3  22880  cayhamlem4  22881  dyadmax  25618  cpnfval  25953  deg1ldg  26119  deg1leb  26122  deg1val  26123  deg1mul3  26143  deg1mul3le  26144  uc1pmon1p  26179  plyval  26220  elply2  26223  plyf  26225  elplyr  26228  plyeq0lem  26237  plyeq0  26238  plypf1  26239  plyaddlem1  26240  plyaddlem  26242  plymullem  26243  coeeulem  26251  coeeq  26254  dgrlem  26256  coeidlem  26264  coeaddlem  26276  coemulc  26282  coe0  26283  coesub  26284  dgradd2  26296  dgrcolem2  26302  plydivlem4  26324  plydiveu  26326  vieta1lem2  26339  taylfval  26386  pserval  26439  dvradcnv  26450  pserdvlem2  26458  abelthlem1  26461  abelthlem3  26463  abelthlem6  26466  logtayl  26687  leibpi  26970  sqff1o  27210  clwwlknonmpo  30022  evl1deg1  33448  evl1deg2  33449  evl1deg3  33450  gsummoncoe1fzo  33465  ply1degltdimlem  33517  evls1fldgencl  33556  eulerpartleme  34197  eulerpartlem1  34201  eulerpartlemt  34205  eulerpartgbij  34206  eulerpartlemr  34208  eulerpartlemmf  34209  eulerpartlemgvv  34210  eulerpartlemgs2  34214  eulerpartlemn  34215  fib0  34233  fib1  34234  fibp1  34235  lpadval  34522  knoppcnlem1  36196  knoppcnlem6  36201  poimirlem32  37353  heiborlem3  37514  aks6d1c1  41814  aks6d1c2lem3  41824  aks6d1c5lem0  41833  aks6d1c5lem3  41835  aks6d1c5lem2  41836  aks6d1c5  41837  sticksstones14  41858  sticksstones20  41864  sticksstones23  41867  aks6d1c6lem1  41868  aks6d1c6lem2  41869  eldiophb  42414  diophrw  42416  hbtlem1  42784  hbtlem7  42786  dgrsub2  42796  mpaaeu  42811  deg1mhm  42865  elrtrclrec  43348  brmptiunrelexpd  43350  brrtrclrec  43364  iunrelexp0  43369  iunrelexpmin2  43379  dfrtrcl3  43400  fvrtrcllb0d  43402  fvrtrcllb0da  43403  fvrtrcllb1d  43404  radcnvrat  43988  binomcxplemrat  44024  binomcxplemnotnn0  44030  expfac  45278  dvnprodlem1  45567  dvnprodlem2  45568  dvnprodlem3  45569  etransclem24  45879  etransclem25  45880  etransclem26  45881  etransclem28  45883  etransclem35  45890  etransclem37  45892  etransclem48  45903  fmtnoinf  47108  nn0mnd  47556  ply1mulgsum  47773  itcovalpclem1  48058  itcovalpclem2  48059  itcovalt2lem1  48063  itcovalt2lem2  48064  ackvalsuc1mpt  48066  ackval0  48068  ackendofnn0  48072  ackvalsucsucval  48076