Theorem nn0ex 12424

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 12419	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12168	. . 3 ⊢ ℕ ∈ V
3		snex 5386	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7700	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444   ∪ cun 3909  {csn 4585  0cc0 11044  ℕcn 12162  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-1cn 11102  ax-addcl 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  nn0ennn  13920  nnenom  13921  fsuppmapnn0fiub0  13934  suppssfz  13935  fsuppmapnn0ub  13936  mptnn0fsupp  13938  mptnn0fsuppr  13940  wrdexg  14465  elovmptnn0wrd  14500  rtrclreclem1  14999  dfrtrclrec2  15000  rtrclreclem2  15001  rtrclreclem4  15003  expcnv  15806  geolim  15812  cvgrat  15825  mertenslem2  15827  bpolylem  15990  eftlub  16053  bitsfval  16369  bitsf  16373  sadfval  16398  smufval  16423  smupf  16424  1arith  16874  ramcl  16976  smndex1ibas  18803  smndex1gbas  18805  smndex1gid  18806  smndex1igid  18807  smndex1mnd  18813  smndex1id  18814  smndex1n0mnd  18815  smndex2dbas  18817  smndex2dnrinv  18818  smndex2hbas  18819  smndex2dlinvh  18820  odfval  19438  fsfnn0gsumfsffz  19889  gsummptnn0fz  19892  nn0srg  21330  psrbag  21802  evlsgsumadd  21974  evlsgsummul  21975  mhpfval  22001  mhpmulcl  22012  coe1fval  22066  fvcoe1  22068  coe1fval3  22069  coe1f2  22070  coe1sfi  22074  coe1fsupp  22075  00ply1bas  22100  ply1plusgfvi  22102  coe1z  22125  coe1add  22126  coe1addfv  22127  coe1mul2lem1  22129  coe1mul2lem2  22130  coe1mul2  22131  coe1tm  22135  coe1sclmul  22144  coe1sclmulfv  22145  coe1sclmul2  22146  ply1coefsupp  22160  ply1coe  22161  gsumsmonply1  22170  gsummoncoe1  22171  evls1gsumadd  22187  evls1gsummul  22188  evl1gsummul  22223  evls1fpws  22232  pmatcollpw1  22639  pmatcollpw2lem  22640  pmatcollpw2  22641  pmatcollpw3lem  22646  pm2mpcl  22660  idpm2idmp  22664  mply1topmatcllem  22666  mply1topmatcl  22668  mp2pm2mplem2  22670  mp2pm2mplem5  22673  mp2pm2mp  22674  pm2mpghmlem2  22675  pm2mpghm  22679  pm2mpmhmlem2  22682  monmat2matmon  22687  pm2mp  22688  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  cpmidpmatlem2  22734  cpmadumatpolylem1  22744  cpmadumatpolylem2  22745  chcoeffeqlem  22748  cayhamlem3  22750  cayhamlem4  22751  dyadmax  25475  cpnfval  25810  deg1ldg  25973  deg1leb  25976  deg1val  25977  deg1mul3  25997  deg1mul3le  25998  uc1pmon1p  26033  plyval  26074  elply2  26077  plyf  26079  elplyr  26082  plyeq0lem  26091  plyeq0  26092  plypf1  26093  plyaddlem1  26094  plyaddlem  26096  plymullem  26097  coeeulem  26105  coeeq  26108  dgrlem  26110  coeidlem  26118  coeaddlem  26130  coemulc  26136  coe0  26137  coesub  26138  dgradd2  26150  dgrcolem2  26156  plydivlem4  26180  plydiveu  26182  vieta1lem2  26195  taylfval  26242  pserval  26295  dvradcnv  26306  pserdvlem2  26314  abelthlem1  26317  abelthlem3  26319  abelthlem6  26322  logtayl  26545  leibpi  26828  sqff1o  27068  clwwlknonmpo  29991  ressply1evls1  33507  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  gsummoncoe1fzo  33536  ply1degltdimlem  33591  evls1fldgencl  33638  eulerpartleme  34327  eulerpartlem1  34331  eulerpartlemt  34335  eulerpartgbij  34336  eulerpartlemr  34338  eulerpartlemmf  34339  eulerpartlemgvv  34340  eulerpartlemgs2  34344  eulerpartlemn  34345  fib0  34363  fib1  34364  fibp1  34365  lpadval  34640  knoppcnlem1  36454  knoppcnlem6  36459  poimirlem32  37619  heiborlem3  37780  aks6d1c1  42077  aks6d1c2lem3  42087  aks6d1c5lem0  42096  aks6d1c5lem3  42098  aks6d1c5lem2  42099  aks6d1c5  42100  sticksstones14  42121  sticksstones20  42127  sticksstones23  42130  aks6d1c6lem1  42131  aks6d1c6lem2  42132  eldiophb  42718  diophrw  42720  hbtlem1  43085  hbtlem7  43087  dgrsub2  43097  mpaaeu  43112  deg1mhm  43162  elrtrclrec  43643  brmptiunrelexpd  43645  brrtrclrec  43659  iunrelexp0  43664  iunrelexpmin2  43674  dfrtrcl3  43695  fvrtrcllb0d  43697  fvrtrcllb0da  43698  fvrtrcllb1d  43699  radcnvrat  44276  binomcxplemrat  44312  binomcxplemnotnn0  44318  expfac  45628  dvnprodlem1  45917  dvnprodlem2  45918  dvnprodlem3  45919  etransclem24  46229  etransclem25  46230  etransclem26  46231  etransclem28  46233  etransclem35  46240  etransclem37  46242  etransclem48  46253  fmtnoinf  47510  nn0mnd  48140  ply1mulgsum  48352  itcovalpclem1  48632  itcovalpclem2  48633  itcovalt2lem1  48637  itcovalt2lem2  48638  ackvalsuc1mpt  48640  ackval0  48642  ackendofnn0  48646  ackvalsucsucval  48650