Theorem nn0ex 12605

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 12600	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12334	. . 3 ⊢ ℕ ∈ V
3		snex 5397	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7759	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2857	1 ⊢ ℕ0 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897  {csn 4584  0cc0 11193  ℕcn 12328  ℕ₀cn0 12599

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-1cn 11251  ax-addcl 11253

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-nn 12329  df-n0 12600

This theorem is used by:  nn0ennn  14115  nnenom  14116  fsuppmapnn0fiub0  14129  suppssfz  14130  fsuppmapnn0ub  14131  mptnn0fsupp  14133  mptnn0fsuppr  14135  wrdexg  14662  elovmptnn0wrd  14697  rtrclreclem1  15203  dfrtrclrec2  15204  rtrclreclem2  15205  rtrclreclem4  15207  expcnv  16026  geolim  16032  cvgrat  16045  mertenslem2  16047  bpolylem  16207  eftlub  16270  bitsfval  16586  bitsf  16590  sadfval  16615  smufval  16640  smupf  16641  1arith  17098  ramcl  17200  smndex1ibas  19089  smndex1gbas  19091  smndex1gbasOLD  19092  smndex1gid  19093  smndex1gidOLD  19094  smndex1igid  19095  smndex1igidOLD  19096  smndex1mnd  19102  smndex1id  19103  smndex1n0mnd  19104  smndex2dbas  19106  smndex2dnrinv  19107  smndex2hbas  19108  smndex2dlinvh  19109  odfval  19739  fsfnn0gsumfsffz  20190  gsummptnn0fz  20193  nn0srg  21736  psrbag  22218  evlsgsumadd  22398  evlsgsummul  22399  mhpfval  22452  mhpmulcl  22463  coe1fval  22516  fvcoe1  22518  coe1fval3  22519  coe1f2  22520  coe1sfi  22524  coe1fsupp  22525  00ply1bas  22550  ply1plusgfvi  22552  coe1z  22575  coe1add  22576  coe1addfv  22577  coe1mul2lem1  22579  coe1mul2lem2  22580  coe1mul2  22581  coe1tm  22585  coe1sclmul  22594  coe1sclmulfv  22595  coe1sclmul2  22596  ply1coefsupp  22608  ply1coe  22609  gsumsmonply1  22618  gsummoncoe1  22619  evls1gsumadd  22635  evls1gsummul  22636  evl1gsummul  22671  evls1fpws  22680  pmatcollpw1  23087  pmatcollpw2lem  23088  pmatcollpw2  23089  pmatcollpw3lem  23094  pm2mpcl  23108  idpm2idmp  23112  mply1topmatcllem  23114  mply1topmatcl  23116  mp2pm2mplem2  23118  mp2pm2mplem5  23121  mp2pm2mp  23122  pm2mpghmlem2  23123  pm2mpghm  23127  pm2mpmhmlem2  23130  monmat2matmon  23135  pm2mp  23136  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  cpmidpmatlem2  23182  cpmadumatpolylem1  23192  cpmadumatpolylem2  23193  chcoeffeqlem  23196  cayhamlem3  23198  cayhamlem4  23199  dyadmax  25912  cpnfval  26245  deg1ldg  26403  deg1leb  26406  deg1val  26407  deg1mul3  26427  deg1mul3le  26428  uc1pmon1p  26463  plyval  26504  elply2  26507  plyf  26509  elplyr  26512  plyeq0lem  26522  plyeq0  26523  plypf1  26524  plyaddlem1  26525  plyaddlem  26527  plymullem  26528  coeeulem  26536  coeeq  26539  dgrlem  26541  coeidlem  26549  coeaddlem  26561  coemulc  26567  coe0  26568  coesub  26569  dgradd2  26580  dgrcolem2  26586  plydivlem4  26610  plydiveu  26612  vieta1lem2  26627  taylfval  26679  pserval  26730  dvradcnv  26741  pserdvlem2  26748  abelthlem1  26751  abelthlem3  26753  abelthlem6  26756  logtayl  26981  leibpi  27263  sqff1o  27502  clwwlknonmpo  30673  ressply1evls1  34090  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  ply1coedeg  34114  gsummoncoe1fzo  34122  0mplrim  34139  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem2  34146  selvply1rhmlem4  34148  selvply1rhm0  34151  mplmulmvr  34164  evlextv  34167  mplvrpmlem  34168  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonprod  34177  esplyval  34187  esplyfval0  34189  esplylem  34191  esplyfv1  34194  esplyfvaln  34199  esplyind  34200  vieta  34205  ply1degltdimlem  34247  evls1fldgencl  34295  extdgfialglem2  34318  eulerpartleme  34988  eulerpartlem1  34992  eulerpartlemt  34996  eulerpartgbij  34997  eulerpartlemr  34999  eulerpartlemmf  35000  eulerpartlemgvv  35001  eulerpartlemgs2  35005  eulerpartlemn  35006  fib0  35024  fib1  35025  fibp1  35026  lpadval  35301  knoppcnlem1  37339  knoppcnlem6  37344  poimirlem32  38550  heiborlem3  38727  aks6d1c1  43146  aks6d1c2lem3  43156  aks6d1c5lem0  43165  aks6d1c5lem3  43167  aks6d1c5lem2  43168  aks6d1c5  43169  sticksstones14  43190  sticksstones20  43196  sticksstones23  43199  aks6d1c6lem1  43200  aks6d1c6lem2  43201  eldiophb  43747  diophrw  43749  hbtlem1  44109  hbtlem7  44111  dgrsub2  44121  mpaaeu  44136  deg1mhm  44186  elrtrclrec  44666  brmptiunrelexpd  44668  brrtrclrec  44682  iunrelexp0  44687  iunrelexpmin2  44697  dfrtrcl3  44718  fvrtrcllb0d  44720  fvrtrcllb0da  44721  fvrtrcllb1d  44722  radcnvrat  45283  binomcxplemrat  45319  binomcxplemnotnn0  45325  expfac  46636  dvnprodlem1  46925  dvnprodlem2  46926  dvnprodlem3  46927  etransclem24  47237  etransclem25  47238  etransclem26  47239  etransclem28  47241  etransclem35  47248  etransclem37  47250  etransclem48  47261  numtowerdt  47885  fmtnoinf  48590  nn0mnd  49245  ply1mulgsum  49471  itcovalpclem1  49751  itcovalpclem2  49752  itcovalt2lem1  49756  itcovalt2lem2  49757  ackvalsuc1mpt  49759  ackval0  49761  ackendofnn0  49765  ackvalsucsucval  49769