Theorem nn0ex 12619

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 12614	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12348	. . 3 ⊢ ℕ ∈ V
3		snex 5397	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7765	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2856	1 ⊢ ℕ0 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∪ cun 4148  {csn 4584  0cc0 11207  ℕcn 12342  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-1cn 11265  ax-addcl 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  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 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7427  df-om 7882  df-2nd 8006  df-frecs 8306  df-wrecs 8337  df-recs 8386  df-rdg 8425  df-nn 12343  df-n0 12614

This theorem is used by:  nn0ennn  14129  nnenom  14130  fsuppmapnn0fiub0  14143  suppssfz  14144  fsuppmapnn0ub  14145  mptnn0fsupp  14147  mptnn0fsuppr  14149  wrdexg  14676  elovmptnn0wrd  14711  rtrclreclem1  15219  dfrtrclrec2  15220  rtrclreclem2  15221  rtrclreclem4  15223  expcnv  16042  geolim  16048  cvgrat  16061  mertenslem2  16063  bpolylem  16223  eftlub  16286  bitsfval  16602  bitsf  16606  sadfval  16631  smufval  16656  smupf  16657  1arith  17114  ramcl  17216  smndex1ibas  19105  smndex1gbas  19107  smndex1gbasOLD  19108  smndex1gid  19109  smndex1gidOLD  19110  smndex1igid  19111  smndex1igidOLD  19112  smndex1mnd  19118  smndex1id  19119  smndex1n0mnd  19120  smndex2dbas  19122  smndex2dnrinv  19123  smndex2hbas  19124  smndex2dlinvh  19125  odfval  19755  fsfnn0gsumfsffz  20206  gsummptnn0fz  20209  nn0srg  21752  psrbag  22234  evlsgsumadd  22414  evlsgsummul  22415  mhpfval  22468  mhpmulcl  22479  coe1fval  22532  fvcoe1  22534  coe1fval3  22535  coe1f2  22536  coe1sfi  22540  coe1fsupp  22541  00ply1bas  22566  ply1plusgfvi  22568  coe1z  22591  coe1add  22592  coe1addfv  22593  coe1mul2lem1  22595  coe1mul2lem2  22596  coe1mul2  22597  coe1tm  22601  coe1sclmul  22610  coe1sclmulfv  22611  coe1sclmul2  22612  ply1coefsupp  22624  ply1coe  22625  gsumsmonply1  22634  gsummoncoe1  22635  evls1gsumadd  22651  evls1gsummul  22652  evl1gsummul  22687  evls1fpws  22696  pmatcollpw1  23103  pmatcollpw2lem  23104  pmatcollpw2  23105  pmatcollpw3lem  23110  pm2mpcl  23124  idpm2idmp  23128  mply1topmatcllem  23130  mply1topmatcl  23132  mp2pm2mplem2  23134  mp2pm2mplem5  23137  mp2pm2mp  23138  pm2mpghmlem2  23139  pm2mpghm  23143  pm2mpmhmlem2  23146  monmat2matmon  23151  pm2mp  23152  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  cpmidpmatlem2  23198  cpmadumatpolylem1  23208  cpmadumatpolylem2  23209  chcoeffeqlem  23212  cayhamlem3  23214  cayhamlem4  23215  dyadmax  25928  cpnfval  26261  deg1ldg  26419  deg1leb  26422  deg1val  26423  deg1mul3  26443  deg1mul3le  26444  uc1pmon1p  26479  plyval  26520  elply2  26523  plyf  26525  elplyr  26528  plyeq0lem  26538  plyeq0  26539  plypf1  26540  plyaddlem1  26541  plyaddlem  26543  plymullem  26544  coeeulem  26552  coeeq  26555  dgrlem  26557  coeidlem  26565  coeaddlem  26577  coemulc  26583  coe0  26584  coesub  26585  dgradd2  26596  dgrcolem2  26602  plydivlem4  26626  plydiveu  26628  vieta1lem2  26643  taylfval  26695  pserval  26746  dvradcnv  26757  pserdvlem2  26764  abelthlem1  26767  abelthlem3  26769  abelthlem6  26772  logtayl  26997  leibpi  27279  sqff1o  27518  clwwlknonmpo  30689  ressply1evls1  34147  evl1deg1  34158  evl1deg2  34159  evl1deg3  34160  ply1coedeg  34171  gsummoncoe1fzo  34179  0mplrim  34196  selvply1rhmlema  34200  selvply1rhmlemb  34201  selvply1rhmlem1  34202  selvply1rhmlem2  34203  selvply1rhmlem4  34205  selvply1rhm0  34208  mplmulmvr  34221  evlextv  34224  mplvrpmlem  34225  mplvrpmfgalem  34226  mplvrpmga  34227  mplvrpmmhm  34228  mplvrpmrhm  34229  psrmonprod  34234  esplyval  34244  esplyfval0  34246  esplylem  34248  esplyfv1  34251  esplyfvaln  34256  esplyind  34257  vieta  34262  ply1degltdimlem  34304  evls1fldgencl  34352  extdgfialglem2  34375  eulerpartleme  35045  eulerpartlem1  35049  eulerpartlemt  35053  eulerpartgbij  35054  eulerpartlemr  35056  eulerpartlemmf  35057  eulerpartlemgvv  35058  eulerpartlemgs2  35062  eulerpartlemn  35063  fib0  35081  fib1  35082  fibp1  35083  lpadval  35358  knoppcnlem1  37455  knoppcnlem6  37460  poimirlem32  38679  heiborlem3  38856  aks6d1c1  43275  aks6d1c2lem3  43285  aks6d1c5lem0  43294  aks6d1c5lem3  43296  aks6d1c5lem2  43297  aks6d1c5  43298  sticksstones14  43319  sticksstones20  43325  sticksstones23  43328  aks6d1c6lem1  43329  aks6d1c6lem2  43330  eldiophb  43877  diophrw  43879  hbtlem1  44234  hbtlem7  44236  dgrsub2  44246  mpaaeu  44261  deg1mhm  44311  elrtrclrec  44790  brmptiunrelexpd  44792  brrtrclrec  44806  iunrelexp0  44811  iunrelexpmin2  44821  dfrtrcl3  44842  fvrtrcllb0d  44844  fvrtrcllb0da  44845  fvrtrcllb1d  44846  radcnvrat  45407  binomcxplemrat  45443  binomcxplemnotnn0  45449  expfac  46775  dvnprodlem1  47064  dvnprodlem2  47065  dvnprodlem3  47066  etransclem24  47376  etransclem25  47377  etransclem26  47378  etransclem28  47380  etransclem35  47387  etransclem37  47389  etransclem48  47400  numtowerdt  48024  fmtnoinf  48729  nn0mnd  49384  ply1mulgsum  49610  itcovalpclem1  49890  itcovalpclem2  49891  itcovalt2lem1  49895  itcovalt2lem2  49896  ackvalsuc1mpt  49898  ackval0  49900  ackendofnn0  49904  ackvalsucsucval  49908