Theorem nn0ex 12481

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 12476	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12210	. . 3 ⊢ ℕ ∈ V
3		snex 5393	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7722	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2857	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 3453   ∪ cun 3900  {csn 4579  0cc0 11067  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-1cn 11125  ax-addcl 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205  df-n0 12476

This theorem is referenced by:  nn0ennn  13986  nnenom  13987  fsuppmapnn0fiub0  14000  suppssfz  14001  fsuppmapnn0ub  14002  mptnn0fsupp  14004  mptnn0fsuppr  14006  wrdexg  14531  elovmptnn0wrd  14566  rtrclreclem1  15064  dfrtrclrec2  15065  rtrclreclem2  15066  rtrclreclem4  15068  expcnv  15885  geolim  15891  cvgrat  15904  mertenslem2  15906  bpolylem  16069  eftlub  16132  bitsfval  16448  bitsf  16452  sadfval  16477  smufval  16502  smupf  16503  1arith  16954  ramcl  17056  smndex1ibas  18925  smndex1gbas  18927  smndex1gbasOLD  18928  smndex1gid  18929  smndex1gidOLD  18930  smndex1igid  18931  smndex1igidOLD  18932  smndex1mnd  18938  smndex1id  18939  smndex1n0mnd  18940  smndex2dbas  18942  smndex2dnrinv  18943  smndex2hbas  18944  smndex2dlinvh  18945  odfval  19563  fsfnn0gsumfsffz  20014  gsummptnn0fz  20017  nn0srg  21477  psrbag  21957  evlsgsumadd  22137  evlsgsummul  22138  mhpfval  22191  mhpmulcl  22202  coe1fval  22255  fvcoe1  22257  coe1fval3  22258  coe1f2  22259  coe1sfi  22263  coe1fsupp  22264  00ply1bas  22289  ply1plusgfvi  22291  coe1z  22314  coe1add  22315  coe1addfv  22316  coe1mul2lem1  22318  coe1mul2lem2  22319  coe1mul2  22320  coe1tm  22324  coe1sclmul  22333  coe1sclmulfv  22334  coe1sclmul2  22335  ply1coefsupp  22348  ply1coe  22349  gsumsmonply1  22358  gsummoncoe1  22359  evls1gsumadd  22375  evls1gsummul  22376  evl1gsummul  22411  evls1fpws  22420  pmatcollpw1  22824  pmatcollpw2lem  22825  pmatcollpw2  22826  pmatcollpw3lem  22831  pm2mpcl  22845  idpm2idmp  22849  mply1topmatcllem  22851  mply1topmatcl  22853  mp2pm2mplem2  22855  mp2pm2mplem5  22858  mp2pm2mp  22859  pm2mpghmlem2  22860  pm2mpghm  22864  pm2mpmhmlem2  22867  monmat2matmon  22872  pm2mp  22873  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  cpmidpmatlem2  22919  cpmadumatpolylem1  22929  cpmadumatpolylem2  22930  chcoeffeqlem  22933  cayhamlem3  22935  cayhamlem4  22936  dyadmax  25648  cpnfval  25982  deg1ldg  26140  deg1leb  26143  deg1val  26144  deg1mul3  26164  deg1mul3le  26165  uc1pmon1p  26200  plyval  26241  elply2  26244  plyf  26246  elplyr  26249  plyeq0lem  26258  plyeq0  26259  plypf1  26260  plyaddlem1  26261  plyaddlem  26263  plymullem  26264  coeeulem  26272  coeeq  26275  dgrlem  26277  coeidlem  26285  coeaddlem  26297  coemulc  26303  coe0  26304  coesub  26305  dgradd2  26316  dgrcolem2  26322  plydivlem4  26348  plydiveu  26350  vieta1lem2  26363  taylfval  26410  pserval  26461  dvradcnv  26472  pserdvlem2  26479  abelthlem1  26482  abelthlem3  26484  abelthlem6  26487  logtayl  26713  leibpi  26995  sqff1o  27234  clwwlknonmpo  30248  ressply1evls1  33722  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  ply1coedeg  33746  gsummoncoe1fzo  33754  0mplrim  33772  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhmlem2  33779  selvply1rhmlem4  33781  selvply1rhm0  33784  extvfvvcl  33793  extvfvcl  33794  mplmulmvr  33797  evlextv  33800  mplvrpmlem  33801  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrmonprod  33810  esplyval  33820  esplyfval0  33822  esplylem  33824  esplymhp  33826  esplyfv1  33827  esplysply  33829  esplyfval3  33830  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  vieta  33838  ply1degltdimlem  33880  evls1fldgencl  33928  extdgfialglem2  33951  eulerpartleme  34621  eulerpartlem1  34625  eulerpartlemt  34629  eulerpartgbij  34630  eulerpartlemr  34632  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgs2  34638  eulerpartlemn  34639  fib0  34657  fib1  34658  fibp1  34659  lpadval  34934  knoppcnlem1  36892  knoppcnlem6  36897  poimirlem32  38112  heiborlem3  38273  aks6d1c1  42694  aks6d1c2lem3  42704  aks6d1c5lem0  42713  aks6d1c5lem3  42715  aks6d1c5lem2  42716  aks6d1c5  42717  sticksstones14  42738  sticksstones20  42744  sticksstones23  42747  aks6d1c6lem1  42748  aks6d1c6lem2  42749  eldiophb  43299  diophrw  43301  hbtlem1  43661  hbtlem7  43663  dgrsub2  43673  mpaaeu  43688  deg1mhm  43738  elrtrclrec  44218  brmptiunrelexpd  44220  brrtrclrec  44234  iunrelexp0  44239  iunrelexpmin2  44249  dfrtrcl3  44270  fvrtrcllb0d  44272  fvrtrcllb0da  44273  fvrtrcllb1d  44274  radcnvrat  44851  binomcxplemrat  44887  binomcxplemnotnn0  44893  expfac  46192  dvnprodlem1  46481  dvnprodlem2  46482  dvnprodlem3  46483  etransclem24  46793  etransclem25  46794  etransclem26  46795  etransclem28  46797  etransclem35  46804  etransclem37  46806  etransclem48  46817  nthrucw  47423  fmtnoinf  48106  nn0mnd  48762  ply1mulgsum  48973  itcovalpclem1  49253  itcovalpclem2  49254  itcovalt2lem1  49258  itcovalt2lem2  49259  ackvalsuc1mpt  49261  ackval0  49263  ackendofnn0  49267  ackvalsucsucval  49271