Theorem nn0ex 11904

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 11899	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 11644	. . 3 ⊢ ℕ ∈ V
3		snex 5332	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7469	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2909	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934  {csn 4567  0cc0 10537  ℕcn 11638  ℕ₀cn0 11898

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-n0 11899

This theorem is referenced by:  nn0ennn  13348  nnenom  13349  fsuppmapnn0fiub0  13362  suppssfz  13363  fsuppmapnn0ub  13364  mptnn0fsupp  13366  mptnn0fsuppr  13368  wrdexg  13872  elovmptnn0wrd  13911  dfrtrclrec2  14416  rtrclreclem1  14417  rtrclreclem2  14418  rtrclreclem4  14420  expcnv  15219  geolim  15226  cvgrat  15239  mertenslem2  15241  bpolylem  15402  eftlub  15462  bitsfval  15772  bitsf  15776  sadfval  15801  smufval  15826  smupf  15827  1arith  16263  ramcl  16365  smndex1ibas  18065  smndex1gbas  18067  smndex1gid  18068  smndex1igid  18069  smndex1mnd  18075  smndex1id  18076  smndex1n0mnd  18077  smndex2dbas  18079  smndex2dnrinv  18080  smndex2hbas  18081  smndex2dlinvh  18082  odfval  18660  fsfnn0gsumfsffz  19103  gsummptnn0fz  19106  psrbag  20144  evlsgsumadd  20304  evlsgsummul  20305  mhpfval  20332  coe1fval  20373  fvcoe1  20375  coe1fval3  20376  coe1f2  20377  coe1sfi  20381  coe1fsupp  20382  00ply1bas  20408  ply1plusgfvi  20410  coe1z  20431  coe1add  20432  coe1addfv  20433  coe1mul2lem1  20435  coe1mul2lem2  20436  coe1mul2  20437  coe1tm  20441  coe1sclmul  20450  coe1sclmulfv  20451  coe1sclmul2  20452  ply1coefsupp  20463  ply1coe  20464  gsumsmonply1  20471  gsummoncoe1  20472  evls1gsumadd  20487  evls1gsummul  20488  evl1gsummul  20523  nn0srg  20615  pmatcollpw1  21384  pmatcollpw2lem  21385  pmatcollpw2  21386  pmatcollpw3lem  21391  pm2mpcl  21405  idpm2idmp  21409  mply1topmatcllem  21411  mply1topmatcl  21413  mp2pm2mplem2  21415  mp2pm2mplem5  21418  mp2pm2mp  21419  pm2mpghmlem2  21420  pm2mpghm  21424  pm2mpmhmlem2  21427  monmat2matmon  21432  pm2mp  21433  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmidpmatlem2  21479  cpmadumatpolylem1  21489  cpmadumatpolylem2  21490  chcoeffeqlem  21493  cayhamlem3  21495  cayhamlem4  21496  dyadmax  24199  cpnfval  24529  deg1ldg  24686  deg1leb  24689  deg1val  24690  deg1mul3  24709  deg1mul3le  24710  uc1pmon1p  24745  plyval  24783  elply2  24786  plyf  24788  elplyr  24791  plyeq0lem  24800  plyeq0  24801  plypf1  24802  plyaddlem1  24803  plyaddlem  24805  plymullem  24806  coeeulem  24814  coeeq  24817  dgrlem  24819  coeidlem  24827  coeaddlem  24839  coemulc  24845  coe0  24846  coesub  24847  dgradd2  24858  dgrcolem2  24864  plydivlem4  24885  plydiveu  24887  vieta1lem2  24900  taylfval  24947  pserval  24998  dvradcnv  25009  pserdvlem2  25016  abelthlem1  25019  abelthlem3  25021  abelthlem6  25024  logtayl  25243  leibpi  25520  sqff1o  25759  clwwlknonmpo  27868  eulerpartleme  31621  eulerpartlem1  31625  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemr  31632  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgs2  31638  eulerpartlemn  31639  fib0  31657  fib1  31658  fibp1  31659  lpadval  31947  knoppcnlem1  33832  knoppcnlem6  33837  poimirlem32  34939  heiborlem3  35106  eldiophb  39374  diophrw  39376  hbtlem1  39743  hbtlem7  39745  dgrsub2  39755  mpaaeu  39770  deg1mhm  39827  elrtrclrec  40046  brmptiunrelexpd  40048  brrtrclrec  40062  iunrelexp0  40067  iunrelexpmin2  40077  dfrtrcl3  40098  fvrtrcllb0d  40100  fvrtrcllb0da  40101  fvrtrcllb1d  40102  radcnvrat  40666  binomcxplemrat  40702  binomcxplemnotnn0  40708  expfac  41958  dvnprodlem1  42251  dvnprodlem2  42252  dvnprodlem3  42253  etransclem24  42563  etransclem25  42564  etransclem26  42565  etransclem28  42567  etransclem35  42574  etransclem37  42576  etransclem48  42587  fmtnoinf  43718  nn0mnd  44106  ply1mulgsum  44464