Theorem nn0ex 12408

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 12403	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12152	. . 3 ⊢ ℕ ∈ V
3		snex 5378	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7684	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∪ cun 3903  {csn 4579  0cc0 11028  ℕcn 12146  ℕ₀cn0 12402

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-1cn 11086  ax-addcl 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147  df-n0 12403

This theorem is referenced by:  nn0ennn  13904  nnenom  13905  fsuppmapnn0fiub0  13918  suppssfz  13919  fsuppmapnn0ub  13920  mptnn0fsupp  13922  mptnn0fsuppr  13924  wrdexg  14449  elovmptnn0wrd  14484  rtrclreclem1  14982  dfrtrclrec2  14983  rtrclreclem2  14984  rtrclreclem4  14986  expcnv  15789  geolim  15795  cvgrat  15808  mertenslem2  15810  bpolylem  15973  eftlub  16036  bitsfval  16352  bitsf  16356  sadfval  16381  smufval  16406  smupf  16407  1arith  16857  ramcl  16959  smndex1ibas  18792  smndex1gbas  18794  smndex1gid  18795  smndex1igid  18796  smndex1mnd  18802  smndex1id  18803  smndex1n0mnd  18804  smndex2dbas  18806  smndex2dnrinv  18807  smndex2hbas  18808  smndex2dlinvh  18809  odfval  19429  fsfnn0gsumfsffz  19880  gsummptnn0fz  19883  nn0srg  21362  psrbag  21842  evlsgsumadd  22014  evlsgsummul  22015  mhpfval  22041  mhpmulcl  22052  coe1fval  22106  fvcoe1  22108  coe1fval3  22109  coe1f2  22110  coe1sfi  22114  coe1fsupp  22115  00ply1bas  22140  ply1plusgfvi  22142  coe1z  22165  coe1add  22166  coe1addfv  22167  coe1mul2lem1  22169  coe1mul2lem2  22170  coe1mul2  22171  coe1tm  22175  coe1sclmul  22184  coe1sclmulfv  22185  coe1sclmul2  22186  ply1coefsupp  22200  ply1coe  22201  gsumsmonply1  22210  gsummoncoe1  22211  evls1gsumadd  22227  evls1gsummul  22228  evl1gsummul  22263  evls1fpws  22272  pmatcollpw1  22679  pmatcollpw2lem  22680  pmatcollpw2  22681  pmatcollpw3lem  22686  pm2mpcl  22700  idpm2idmp  22704  mply1topmatcllem  22706  mply1topmatcl  22708  mp2pm2mplem2  22710  mp2pm2mplem5  22713  mp2pm2mp  22714  pm2mpghmlem2  22715  pm2mpghm  22719  pm2mpmhmlem2  22722  monmat2matmon  22727  pm2mp  22728  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  cpmidpmatlem2  22774  cpmadumatpolylem1  22784  cpmadumatpolylem2  22785  chcoeffeqlem  22788  cayhamlem3  22790  cayhamlem4  22791  dyadmax  25515  cpnfval  25850  deg1ldg  26013  deg1leb  26016  deg1val  26017  deg1mul3  26037  deg1mul3le  26038  uc1pmon1p  26073  plyval  26114  elply2  26117  plyf  26119  elplyr  26122  plyeq0lem  26131  plyeq0  26132  plypf1  26133  plyaddlem1  26134  plyaddlem  26136  plymullem  26137  coeeulem  26145  coeeq  26148  dgrlem  26150  coeidlem  26158  coeaddlem  26170  coemulc  26176  coe0  26177  coesub  26178  dgradd2  26190  dgrcolem2  26196  plydivlem4  26220  plydiveu  26222  vieta1lem2  26235  taylfval  26282  pserval  26335  dvradcnv  26346  pserdvlem2  26354  abelthlem1  26357  abelthlem3  26359  abelthlem6  26362  logtayl  26585  leibpi  26868  sqff1o  27108  clwwlknonmpo  30051  ressply1evls1  33513  evl1deg1  33524  evl1deg2  33525  evl1deg3  33526  gsummoncoe1fzo  33542  ply1degltdimlem  33597  evls1fldgencl  33644  eulerpartleme  34333  eulerpartlem1  34337  eulerpartlemt  34341  eulerpartgbij  34342  eulerpartlemr  34344  eulerpartlemmf  34345  eulerpartlemgvv  34346  eulerpartlemgs2  34350  eulerpartlemn  34351  fib0  34369  fib1  34370  fibp1  34371  lpadval  34646  knoppcnlem1  36469  knoppcnlem6  36474  poimirlem32  37634  heiborlem3  37795  aks6d1c1  42092  aks6d1c2lem3  42102  aks6d1c5lem0  42111  aks6d1c5lem3  42113  aks6d1c5lem2  42114  aks6d1c5  42115  sticksstones14  42136  sticksstones20  42142  sticksstones23  42145  aks6d1c6lem1  42146  aks6d1c6lem2  42147  eldiophb  42733  diophrw  42735  hbtlem1  43099  hbtlem7  43101  dgrsub2  43111  mpaaeu  43126  deg1mhm  43176  elrtrclrec  43657  brmptiunrelexpd  43659  brrtrclrec  43673  iunrelexp0  43678  iunrelexpmin2  43688  dfrtrcl3  43709  fvrtrcllb0d  43711  fvrtrcllb0da  43712  fvrtrcllb1d  43713  radcnvrat  44290  binomcxplemrat  44326  binomcxplemnotnn0  44332  expfac  45642  dvnprodlem1  45931  dvnprodlem2  45932  dvnprodlem3  45933  etransclem24  46243  etransclem25  46244  etransclem26  46245  etransclem28  46247  etransclem35  46254  etransclem37  46256  etransclem48  46267  fmtnoinf  47524  nn0mnd  48167  ply1mulgsum  48379  itcovalpclem1  48659  itcovalpclem2  48660  itcovalt2lem1  48664  itcovalt2lem2  48665  ackvalsuc1mpt  48667  ackval0  48669  ackendofnn0  48673  ackvalsucsucval  48677