Theorem nn0ex 11712

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 11706	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 11444	. . 3 ⊢ ℕ ∈ V
3		snex 5184	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7284	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2855	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2051  Vcvv 3408   ∪ cun 3820  {csn 4435  0cc0 10333  ℕcn 11437  ℕ₀cn0 11705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-1cn 10391  ax-addcl 10393

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-ov 6977  df-om 7395  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-nn 11438  df-n0 11706

This theorem is referenced by:  nn0ennn  13160  nnenom  13161  fsuppmapnn0fiub0  13174  suppssfz  13175  fsuppmapnn0ub  13176  mptnn0fsupp  13178  mptnn0fsuppr  13180  wrdexg  13680  elovmptnn0wrd  13720  dfrtrclrec2  14275  rtrclreclem1  14276  rtrclreclem2  14277  rtrclreclem4  14279  expcnv  15077  geolim  15084  cvgrat  15097  mertenslem2  15099  bpolylem  15260  eftlub  15320  bitsfval  15630  bitsf  15634  sadfval  15659  smufval  15684  smupf  15685  1arith  16117  ramcl  16219  odfval  18434  fsfnn0gsumfsffz  18865  gsummptnn0fz  18868  psrbag  19870  mhpfval  20050  coe1fval  20091  fvcoe1  20093  coe1fval3  20094  coe1f2  20095  coe1sfi  20099  coe1fsupp  20100  00ply1bas  20126  ply1plusgfvi  20128  coe1z  20149  coe1add  20150  coe1addfv  20151  coe1mul2lem1  20153  coe1mul2lem2  20154  coe1mul2  20155  coe1tm  20159  coe1sclmul  20168  coe1sclmulfv  20169  coe1sclmul2  20170  ply1coefsupp  20181  ply1coe  20182  gsumsmonply1  20189  gsummoncoe1  20190  evls1gsumadd  20205  evls1gsummul  20206  evl1gsummul  20240  nn0srg  20332  pmatcollpw1  21103  pmatcollpw2lem  21104  pmatcollpw2  21105  pmatcollpw3lem  21110  pm2mpcl  21124  idpm2idmp  21128  mply1topmatcllem  21130  mply1topmatcl  21132  mp2pm2mplem2  21134  mp2pm2mplem5  21137  mp2pm2mp  21138  pm2mpghmlem2  21139  pm2mpghm  21143  pm2mpmhmlem2  21146  monmat2matmon  21151  pm2mp  21152  chfacfscmulgsum  21187  chfacfpmmulgsum  21191  cpmidpmatlem2  21198  cpmadumatpolylem1  21208  cpmadumatpolylem2  21209  chcoeffeqlem  21212  cayhamlem3  21214  cayhamlem4  21215  dyadmax  23917  cpnfval  24247  deg1ldg  24404  deg1leb  24407  deg1val  24408  deg1mul3  24427  deg1mul3le  24428  uc1pmon1p  24463  plyval  24501  elply2  24504  plyf  24506  elplyr  24509  plyeq0lem  24518  plyeq0  24519  plypf1  24520  plyaddlem1  24521  plyaddlem  24523  plymullem  24524  coeeulem  24532  coeeq  24535  dgrlem  24537  coeidlem  24545  coeaddlem  24557  coemulc  24563  coe0  24564  coesub  24565  dgradd2  24576  dgrcolem2  24582  plydivlem4  24603  plydiveu  24605  vieta1lem2  24618  taylfval  24665  pserval  24716  dvradcnv  24727  pserdvlem2  24734  abelthlem1  24737  abelthlem3  24739  abelthlem6  24742  logtayl  24959  leibpi  25237  sqff1o  25476  clwwlknonmpo  27632  eulerpartleme  31298  eulerpartlem1  31302  eulerpartlemt  31306  eulerpartgbij  31307  eulerpartlemr  31309  eulerpartlemmf  31310  eulerpartlemgvv  31311  eulerpartlemgs2  31315  eulerpartlemn  31316  fib0  31335  fib1  31336  fibp1  31337  lpadval  31627  knoppcnlem1  33389  knoppcnlem6  33394  poimirlem32  34402  heiborlem3  34570  eldiophb  38787  diophrw  38789  hbtlem1  39157  hbtlem7  39159  dgrsub2  39169  mpaaeu  39184  deg1mhm  39241  elrtrclrec  39427  brmptiunrelexpd  39429  brrtrclrec  39443  iunrelexp0  39448  iunrelexpmin2  39458  dfrtrcl3  39479  fvrtrcllb0d  39481  fvrtrcllb0da  39482  fvrtrcllb1d  39483  radcnvrat  40100  binomcxplemrat  40136  binomcxplemnotnn0  40142  expfac  41403  dvnprodlem1  41695  dvnprodlem2  41696  dvnprodlem3  41697  etransclem24  42008  etransclem25  42009  etransclem26  42010  etransclem28  42012  etransclem35  42019  etransclem37  42021  etransclem48  42032  fmtnoinf  43100  ply1mulgsum  43845