Theorem nn0ex 12222

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 12217	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 11962	. . 3 ⊢ ℕ ∈ V
3		snex 5357	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7587	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2836	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3430   ∪ cun 3889  {csn 4566  0cc0 10855  ℕcn 11956  ℕ₀cn0 12216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-cnex 10911  ax-1cn 10913  ax-addcl 10915

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-nn 11957  df-n0 12217

This theorem is referenced by:  nn0ennn  13680  nnenom  13681  fsuppmapnn0fiub0  13694  suppssfz  13695  fsuppmapnn0ub  13696  mptnn0fsupp  13698  mptnn0fsuppr  13700  wrdexg  14208  elovmptnn0wrd  14243  rtrclreclem1  14749  dfrtrclrec2  14750  rtrclreclem2  14751  rtrclreclem4  14753  expcnv  15557  geolim  15563  cvgrat  15576  mertenslem2  15578  bpolylem  15739  eftlub  15799  bitsfval  16111  bitsf  16115  sadfval  16140  smufval  16165  smupf  16166  1arith  16609  ramcl  16711  smndex1ibas  18520  smndex1gbas  18522  smndex1gid  18523  smndex1igid  18524  smndex1mnd  18530  smndex1id  18531  smndex1n0mnd  18532  smndex2dbas  18534  smndex2dnrinv  18535  smndex2hbas  18536  smndex2dlinvh  18537  odfval  19121  fsfnn0gsumfsffz  19565  gsummptnn0fz  19568  nn0srg  20649  psrbag  21101  evlsgsumadd  21282  evlsgsummul  21283  mhpfval  21310  mhpmulcl  21320  coe1fval  21357  fvcoe1  21359  coe1fval3  21360  coe1f2  21361  coe1sfi  21365  coe1fsupp  21366  00ply1bas  21392  ply1plusgfvi  21394  coe1z  21415  coe1add  21416  coe1addfv  21417  coe1mul2lem1  21419  coe1mul2lem2  21420  coe1mul2  21421  coe1tm  21425  coe1sclmul  21434  coe1sclmulfv  21435  coe1sclmul2  21436  ply1coefsupp  21447  ply1coe  21448  gsumsmonply1  21455  gsummoncoe1  21456  evls1gsumadd  21471  evls1gsummul  21472  evl1gsummul  21507  pmatcollpw1  21906  pmatcollpw2lem  21907  pmatcollpw2  21908  pmatcollpw3lem  21913  pm2mpcl  21927  idpm2idmp  21931  mply1topmatcllem  21933  mply1topmatcl  21935  mp2pm2mplem2  21937  mp2pm2mplem5  21940  mp2pm2mp  21941  pm2mpghmlem2  21942  pm2mpghm  21946  pm2mpmhmlem2  21949  monmat2matmon  21954  pm2mp  21955  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  cpmidpmatlem2  22001  cpmadumatpolylem1  22011  cpmadumatpolylem2  22012  chcoeffeqlem  22015  cayhamlem3  22017  cayhamlem4  22018  dyadmax  24743  cpnfval  25077  deg1ldg  25238  deg1leb  25241  deg1val  25242  deg1mul3  25261  deg1mul3le  25262  uc1pmon1p  25297  plyval  25335  elply2  25338  plyf  25340  elplyr  25343  plyeq0lem  25352  plyeq0  25353  plypf1  25354  plyaddlem1  25355  plyaddlem  25357  plymullem  25358  coeeulem  25366  coeeq  25369  dgrlem  25371  coeidlem  25379  coeaddlem  25391  coemulc  25397  coe0  25398  coesub  25399  dgradd2  25410  dgrcolem2  25416  plydivlem4  25437  plydiveu  25439  vieta1lem2  25452  taylfval  25499  pserval  25550  dvradcnv  25561  pserdvlem2  25568  abelthlem1  25571  abelthlem3  25573  abelthlem6  25576  logtayl  25796  leibpi  26073  sqff1o  26312  clwwlknonmpo  28432  eulerpartleme  32309  eulerpartlem1  32313  eulerpartlemt  32317  eulerpartgbij  32318  eulerpartlemr  32320  eulerpartlemmf  32321  eulerpartlemgvv  32322  eulerpartlemgs2  32326  eulerpartlemn  32327  fib0  32345  fib1  32346  fibp1  32347  lpadval  32635  knoppcnlem1  34652  knoppcnlem6  34657  poimirlem32  35788  heiborlem3  35950  sticksstones14  40096  sticksstones20  40102  eldiophb  40559  diophrw  40561  hbtlem1  40928  hbtlem7  40930  dgrsub2  40940  mpaaeu  40955  deg1mhm  41012  elrtrclrec  41242  brmptiunrelexpd  41244  brrtrclrec  41258  iunrelexp0  41263  iunrelexpmin2  41273  dfrtrcl3  41294  fvrtrcllb0d  41296  fvrtrcllb0da  41297  fvrtrcllb1d  41298  radcnvrat  41885  binomcxplemrat  41921  binomcxplemnotnn0  41927  expfac  43152  dvnprodlem1  43441  dvnprodlem2  43442  dvnprodlem3  43443  etransclem24  43753  etransclem25  43754  etransclem26  43755  etransclem28  43757  etransclem35  43764  etransclem37  43766  etransclem48  43777  fmtnoinf  44940  nn0mnd  45325  ply1mulgsum  45683  itcovalpclem1  45968  itcovalpclem2  45969  itcovalt2lem1  45973  itcovalt2lem2  45974  ackvalsuc1mpt  45976  ackval0  45978  ackendofnn0  45982  ackvalsucsucval  45986