Theorem nn0ex 12312

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 12307	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12052	. . 3 ⊢ ℕ ∈ V
3		snex 5369	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7636	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2834	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3441   ∪ cun 3895  {csn 4571  0cc0 10944  ℕcn 12046  ℕ₀cn0 12306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-1cn 11002  ax-addcl 11004

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-ov 7318  df-om 7758  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-nn 12047  df-n0 12307

This theorem is referenced by:  nn0ennn  13772  nnenom  13773  fsuppmapnn0fiub0  13786  suppssfz  13787  fsuppmapnn0ub  13788  mptnn0fsupp  13790  mptnn0fsuppr  13792  wrdexg  14299  elovmptnn0wrd  14334  rtrclreclem1  14840  dfrtrclrec2  14841  rtrclreclem2  14842  rtrclreclem4  14844  expcnv  15648  geolim  15654  cvgrat  15667  mertenslem2  15669  bpolylem  15830  eftlub  15890  bitsfval  16202  bitsf  16206  sadfval  16231  smufval  16256  smupf  16257  1arith  16698  ramcl  16800  smndex1ibas  18608  smndex1gbas  18610  smndex1gid  18611  smndex1igid  18612  smndex1mnd  18618  smndex1id  18619  smndex1n0mnd  18620  smndex2dbas  18622  smndex2dnrinv  18623  smndex2hbas  18624  smndex2dlinvh  18625  odfval  19209  fsfnn0gsumfsffz  19652  gsummptnn0fz  19655  nn0srg  20740  psrbag  21192  evlsgsumadd  21373  evlsgsummul  21374  mhpfval  21401  mhpmulcl  21411  coe1fval  21448  fvcoe1  21450  coe1fval3  21451  coe1f2  21452  coe1sfi  21456  coe1fsupp  21457  00ply1bas  21483  ply1plusgfvi  21485  coe1z  21506  coe1add  21507  coe1addfv  21508  coe1mul2lem1  21510  coe1mul2lem2  21511  coe1mul2  21512  coe1tm  21516  coe1sclmul  21525  coe1sclmulfv  21526  coe1sclmul2  21527  ply1coefsupp  21538  ply1coe  21539  gsumsmonply1  21546  gsummoncoe1  21547  evls1gsumadd  21562  evls1gsummul  21563  evl1gsummul  21598  pmatcollpw1  21997  pmatcollpw2lem  21998  pmatcollpw2  21999  pmatcollpw3lem  22004  pm2mpcl  22018  idpm2idmp  22022  mply1topmatcllem  22024  mply1topmatcl  22026  mp2pm2mplem2  22028  mp2pm2mplem5  22031  mp2pm2mp  22032  pm2mpghmlem2  22033  pm2mpghm  22037  pm2mpmhmlem2  22040  monmat2matmon  22045  pm2mp  22046  chfacfscmulgsum  22081  chfacfpmmulgsum  22085  cpmidpmatlem2  22092  cpmadumatpolylem1  22102  cpmadumatpolylem2  22103  chcoeffeqlem  22106  cayhamlem3  22108  cayhamlem4  22109  dyadmax  24834  cpnfval  25168  deg1ldg  25329  deg1leb  25332  deg1val  25333  deg1mul3  25352  deg1mul3le  25353  uc1pmon1p  25388  plyval  25426  elply2  25429  plyf  25431  elplyr  25434  plyeq0lem  25443  plyeq0  25444  plypf1  25445  plyaddlem1  25446  plyaddlem  25448  plymullem  25449  coeeulem  25457  coeeq  25460  dgrlem  25462  coeidlem  25470  coeaddlem  25482  coemulc  25488  coe0  25489  coesub  25490  dgradd2  25501  dgrcolem2  25507  plydivlem4  25528  plydiveu  25530  vieta1lem2  25543  taylfval  25590  pserval  25641  dvradcnv  25652  pserdvlem2  25659  abelthlem1  25662  abelthlem3  25664  abelthlem6  25667  logtayl  25887  leibpi  26164  sqff1o  26403  clwwlknonmpo  28562  eulerpartleme  32436  eulerpartlem1  32440  eulerpartlemt  32444  eulerpartgbij  32445  eulerpartlemr  32447  eulerpartlemmf  32448  eulerpartlemgvv  32449  eulerpartlemgs2  32453  eulerpartlemn  32454  fib0  32472  fib1  32473  fibp1  32474  lpadval  32762  knoppcnlem1  34731  knoppcnlem6  34736  poimirlem32  35865  heiborlem3  36027  sticksstones14  40324  sticksstones20  40330  eldiophb  40782  diophrw  40784  hbtlem1  41152  hbtlem7  41154  dgrsub2  41164  mpaaeu  41179  deg1mhm  41236  elrtrclrec  41510  brmptiunrelexpd  41512  brrtrclrec  41526  iunrelexp0  41531  iunrelexpmin2  41541  dfrtrcl3  41562  fvrtrcllb0d  41564  fvrtrcllb0da  41565  fvrtrcllb1d  41566  radcnvrat  42153  binomcxplemrat  42189  binomcxplemnotnn0  42195  expfac  43435  dvnprodlem1  43724  dvnprodlem2  43725  dvnprodlem3  43726  etransclem24  44036  etransclem25  44037  etransclem26  44038  etransclem28  44040  etransclem35  44047  etransclem37  44049  etransclem48  44060  fmtnoinf  45240  nn0mnd  45625  ply1mulgsum  45983  itcovalpclem1  46268  itcovalpclem2  46269  itcovalt2lem1  46273  itcovalt2lem2  46274  ackvalsuc1mpt  46276  ackval0  46278  ackendofnn0  46282  ackvalsucsucval  46286