Theorem nn0ex 12505

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 12500	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12234	. . 3 ⊢ ℕ ∈ V
3		snex 5410	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7742	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2859	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∪ cun 3903  {csn 4589  0cc0 11095  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  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 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12229  df-n0 12500

This theorem is referenced by:  nn0ennn  14011  nnenom  14012  fsuppmapnn0fiub0  14025  suppssfz  14026  fsuppmapnn0ub  14027  mptnn0fsupp  14029  mptnn0fsuppr  14031  wrdexg  14557  elovmptnn0wrd  14592  rtrclreclem1  15090  dfrtrclrec2  15091  rtrclreclem2  15092  rtrclreclem4  15094  expcnv  15914  geolim  15920  cvgrat  15933  mertenslem2  15935  bpolylem  16097  eftlub  16160  bitsfval  16476  bitsf  16480  sadfval  16505  smufval  16530  smupf  16531  1arith  16982  ramcl  17084  smndex1ibas  18954  smndex1gbas  18956  smndex1gbasOLD  18957  smndex1gid  18958  smndex1gidOLD  18959  smndex1igid  18960  smndex1igidOLD  18961  smndex1mnd  18967  smndex1id  18968  smndex1n0mnd  18969  smndex2dbas  18971  smndex2dnrinv  18972  smndex2hbas  18973  smndex2dlinvh  18974  odfval  19597  fsfnn0gsumfsffz  20048  gsummptnn0fz  20051  nn0srg  21587  psrbag  22067  evlsgsumadd  22247  evlsgsummul  22248  mhpfval  22301  mhpmulcl  22312  coe1fval  22365  fvcoe1  22367  coe1fval3  22368  coe1f2  22369  coe1sfi  22373  coe1fsupp  22374  00ply1bas  22399  ply1plusgfvi  22401  coe1z  22424  coe1add  22425  coe1addfv  22426  coe1mul2lem1  22428  coe1mul2lem2  22429  coe1mul2  22430  coe1tm  22434  coe1sclmul  22443  coe1sclmulfv  22444  coe1sclmul2  22445  ply1coefsupp  22457  ply1coe  22458  gsumsmonply1  22467  gsummoncoe1  22468  evls1gsumadd  22484  evls1gsummul  22485  evl1gsummul  22520  evls1fpws  22529  pmatcollpw1  22933  pmatcollpw2lem  22934  pmatcollpw2  22935  pmatcollpw3lem  22940  pm2mpcl  22954  idpm2idmp  22958  mply1topmatcllem  22960  mply1topmatcl  22962  mp2pm2mplem2  22964  mp2pm2mplem5  22967  mp2pm2mp  22968  pm2mpghmlem2  22969  pm2mpghm  22973  pm2mpmhmlem2  22976  monmat2matmon  22981  pm2mp  22982  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  cpmidpmatlem2  23028  cpmadumatpolylem1  23038  cpmadumatpolylem2  23039  chcoeffeqlem  23042  cayhamlem3  23044  cayhamlem4  23045  dyadmax  25757  cpnfval  26091  deg1ldg  26249  deg1leb  26252  deg1val  26253  deg1mul3  26273  deg1mul3le  26274  uc1pmon1p  26309  plyval  26350  elply2  26353  plyf  26355  elplyr  26358  plyeq0lem  26367  plyeq0  26368  plypf1  26369  plyaddlem1  26370  plyaddlem  26372  plymullem  26373  coeeulem  26381  coeeq  26384  dgrlem  26386  coeidlem  26394  coeaddlem  26406  coemulc  26412  coe0  26413  coesub  26414  dgradd2  26425  dgrcolem2  26431  plydivlem4  26457  plydiveu  26459  vieta1lem2  26472  taylfval  26522  pserval  26573  dvradcnv  26584  pserdvlem2  26591  abelthlem1  26594  abelthlem3  26596  abelthlem6  26599  logtayl  26825  leibpi  27107  sqff1o  27346  clwwlknonmpo  30440  ressply1evls1  33855  evl1deg1  33866  evl1deg2  33867  evl1deg3  33868  ply1coedeg  33879  gsummoncoe1fzo  33887  0mplrim  33904  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhmlem2  33911  selvply1rhmlem4  33913  selvply1rhm0  33916  extvfvvcl  33925  extvfvcl  33926  mplmulmvr  33929  evlextv  33932  mplvrpmlem  33933  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmmhm  33936  mplvrpmrhm  33937  psrmonprod  33942  esplyval  33952  esplyfval0  33954  esplylem  33956  esplymhp  33958  esplyfv1  33959  esplysply  33961  esplyfval3  33962  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  vieta  33970  ply1degltdimlem  34012  evls1fldgencl  34060  extdgfialglem2  34083  eulerpartleme  34753  eulerpartlem1  34757  eulerpartlemt  34761  eulerpartgbij  34762  eulerpartlemr  34764  eulerpartlemmf  34765  eulerpartlemgvv  34766  eulerpartlemgs2  34770  eulerpartlemn  34771  fib0  34789  fib1  34790  fibp1  34791  lpadval  35066  knoppcnlem1  37082  knoppcnlem6  37087  poimirlem32  38303  heiborlem3  38464  aks6d1c1  42883  aks6d1c2lem3  42893  aks6d1c5lem0  42902  aks6d1c5lem3  42904  aks6d1c5lem2  42905  aks6d1c5  42906  sticksstones14  42927  sticksstones20  42933  sticksstones23  42936  aks6d1c6lem1  42937  aks6d1c6lem2  42938  eldiophb  43488  diophrw  43490  hbtlem1  43850  hbtlem7  43852  dgrsub2  43862  mpaaeu  43877  deg1mhm  43927  elrtrclrec  44407  brmptiunrelexpd  44409  brrtrclrec  44423  iunrelexp0  44428  iunrelexpmin2  44438  dfrtrcl3  44459  fvrtrcllb0d  44461  fvrtrcllb0da  44462  fvrtrcllb1d  44463  radcnvrat  45024  binomcxplemrat  45060  binomcxplemnotnn0  45066  expfac  46371  dvnprodlem1  46660  dvnprodlem2  46661  dvnprodlem3  46662  etransclem24  46972  etransclem25  46973  etransclem26  46974  etransclem28  46976  etransclem35  46983  etransclem37  46985  etransclem48  46996  nthrucw  47607  fmtnoinf  48288  nn0mnd  48944  ply1mulgsum  49170  itcovalpclem1  49450  itcovalpclem2  49451  itcovalt2lem1  49455  itcovalt2lem2  49456  ackvalsuc1mpt  49458  ackval0  49460  ackendofnn0  49464  ackvalsucsucval  49468