Theorem nn0ex 11585

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 11580	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 11322	. . 3 ⊢ ℕ ∈ V
3		snex 5111	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7196	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2892	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2157  Vcvv 3402   ∪ cun 3778  {csn 4381  0cc0 10231  ℕcn 11315  ℕ₀cn0 11579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-cnex 10287  ax-1cn 10289  ax-addcl 10291

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-om 7306  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-nn 11316  df-n0 11580

This theorem is referenced by:  nn0ennn  13022  nnenom  13023  fsuppmapnn0fiub0  13036  suppssfz  13037  fsuppmapnn0ub  13038  mptnn0fsupp  13040  mptnn0fsuppr  13042  elovmptnn0wrd  13580  dfrtrclrec2  14040  rtrclreclem1  14041  rtrclreclem2  14042  rtrclreclem4  14044  expcnv  14838  geolim  14843  cvgrat  14856  mertenslem2  14858  bpolylem  15019  eftlub  15079  bitsfval  15384  bitsf  15388  sadfval  15413  smufval  15438  smupf  15439  1arith  15868  ramcl  15970  fsfnn0gsumfsffz  18600  gsummptnn0fz  18603  gsummptnn0fzOLD  18604  psrbag  19593  coe1fval  19803  fvcoe1  19805  coe1fval3  19806  coe1f2  19807  coe1sfi  19811  coe1fsupp  19812  00ply1bas  19838  ply1plusgfvi  19840  coe1z  19861  coe1add  19862  coe1addfv  19863  coe1mul2lem1  19865  coe1mul2lem2  19866  coe1mul2  19867  coe1tm  19871  coe1sclmul  19880  coe1sclmulfv  19881  coe1sclmul2  19882  ply1coefsupp  19893  ply1coe  19894  gsumsmonply1  19901  gsummoncoe1  19902  evls1gsumadd  19917  evls1gsummul  19918  evl1gsummul  19952  nn0srg  20044  pmatcollpw1  20815  pmatcollpw2lem  20816  pmatcollpw2  20817  pmatcollpw3lem  20822  pm2mpcl  20836  idpm2idmp  20840  mply1topmatcllem  20842  mply1topmatcl  20844  mp2pm2mplem2  20846  mp2pm2mplem5  20849  mp2pm2mp  20850  pm2mpghmlem2  20851  pm2mpghm  20855  pm2mpmhmlem2  20858  monmat2matmon  20863  pm2mp  20864  chfacfscmulgsum  20899  chfacfpmmulgsum  20903  cpmidpmatlem2  20910  cpmadumatpolylem1  20920  cpmadumatpolylem2  20921  chcoeffeqlem  20924  cayhamlem3  20926  cayhamlem4  20927  dyadmax  23602  cpnfval  23932  deg1ldg  24089  deg1leb  24092  deg1val  24093  deg1mul3  24112  deg1mul3le  24113  uc1pmon1p  24148  plyval  24186  elply2  24189  plyf  24191  elplyr  24194  plyeq0lem  24203  plyeq0  24204  plypf1  24205  plyaddlem1  24206  plyaddlem  24208  plymullem  24209  coeeulem  24217  coeeq  24220  dgrlem  24222  coeidlem  24230  coeaddlem  24242  coemulc  24248  coe0  24249  coesub  24250  dgradd2  24261  dgrcolem2  24267  plydivlem4  24288  plydiveu  24290  vieta1lem2  24303  taylfval  24350  pserval  24401  dvradcnv  24412  pserdvlem2  24419  abelthlem1  24422  abelthlem3  24424  abelthlem6  24427  logtayl  24643  leibpi  24906  sqff1o  25145  clwwlknonmpt2  27277  eulerpartleme  30773  eulerpartlem1  30777  eulerpartlemt  30781  eulerpartgbij  30782  eulerpartlemr  30784  eulerpartlemmf  30785  eulerpartlemgvv  30786  eulerpartlemgs2  30790  eulerpartlemn  30791  fib0  30809  fib1  30810  fibp1  30811  knoppcnlem1  32822  knoppcnlem6  32827  poimirlem32  33773  heiborlem3  33942  eldiophb  37840  diophrw  37842  hbtlem1  38212  hbtlem7  38214  dgrsub2  38224  mpaaeu  38239  deg1mhm  38304  elrtrclrec  38491  brmptiunrelexpd  38493  brrtrclrec  38507  iunrelexp0  38512  iunrelexpmin2  38522  dfrtrcl3  38543  fvrtrcllb0d  38545  fvrtrcllb0da  38546  fvrtrcllb1d  38547  radcnvrat  39031  binomcxplemrat  39067  binomcxplemnotnn0  39073  expfac  40387  dvnprodlem1  40659  dvnprodlem2  40660  dvnprodlem3  40661  etransclem24  40972  etransclem25  40973  etransclem26  40974  etransclem28  40976  etransclem35  40983  etransclem37  40985  etransclem48  40996  fmtnoinf  42041  ply1mulgsum  42764