Theorem nn0ex 11175

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 11170	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 10903	. . 3 ⊢ ℕ ∈ V
3		snex 4835	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 6854	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2684	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538  {csn 4125  0cc0 9815  ℕcn 10897  ℕ₀cn0 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898  df-n0 11170

This theorem is referenced by:  nn0ennn  12640  nnenom  12641  fsuppmapnn0fiub0  12655  suppssfz  12656  fsuppmapnn0ub  12657  mptnn0fsupp  12659  mptnn0fsuppr  12661  elovmptnn0wrd  13203  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649  expcnv  14435  geolim  14440  cvgrat  14454  mertenslem2  14456  bpolylem  14618  eftlub  14678  bitsfval  14983  bitsf  14987  sadfval  15012  smufval  15037  smupf  15038  1arith  15469  ramcl  15571  fsfnn0gsumfsffz  18202  gsummptnn0fz  18205  psrbag  19185  coe1fval  19396  fvcoe1  19398  coe1fval3  19399  coe1f2  19400  coe1sfi  19404  coe1fsupp  19405  00ply1bas  19431  ply1plusgfvi  19433  coe1z  19454  coe1add  19455  coe1addfv  19456  coe1mul2lem1  19458  coe1mul2lem2  19459  coe1mul2  19460  coe1tm  19464  coe1sclmul  19473  coe1sclmulfv  19474  coe1sclmul2  19475  ply1coefsupp  19486  ply1coe  19487  gsumsmonply1  19494  gsummoncoe1  19495  evls1gsumadd  19510  evls1gsummul  19511  evl1gsummul  19545  nn0srg  19635  pmatcollpw1  20400  pmatcollpw2lem  20401  pmatcollpw2  20402  pmatcollpw3lem  20407  pm2mpcl  20421  idpm2idmp  20425  mply1topmatcllem  20427  mply1topmatcl  20429  mp2pm2mplem2  20431  mp2pm2mplem5  20434  mp2pm2mp  20435  pm2mpghmlem2  20436  pm2mpghm  20440  pm2mpmhmlem2  20443  monmat2matmon  20448  pm2mp  20449  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  cpmidpmatlem2  20495  cpmadumatpolylem1  20505  cpmadumatpolylem2  20506  chcoeffeqlem  20509  cayhamlem3  20511  cayhamlem4  20512  dyadmax  23172  cpnfval  23501  deg1ldg  23656  deg1leb  23659  deg1val  23660  deg1mul3  23679  deg1mul3le  23680  uc1pmon1p  23715  plyval  23753  elply2  23756  plyf  23758  elplyr  23761  plyeq0lem  23770  plyeq0  23771  plypf1  23772  plyaddlem1  23773  plyaddlem  23775  plymullem  23776  coeeulem  23784  coeeq  23787  dgrlem  23789  coeidlem  23797  coeaddlem  23809  coemulc  23815  coe0  23816  coesub  23817  dgradd2  23828  dgrcolem2  23834  plydivlem4  23855  plydiveu  23857  vieta1lem2  23870  taylfval  23917  pserval  23968  dvradcnv  23979  pserdvlem2  23986  abelthlem1  23989  abelthlem3  23991  abelthlem6  23994  logtayl  24206  leibpi  24469  sqff1o  24708  wwlkn  26210  clwwlkn  26295  clwwlknprop  26300  iseupa  26492  eulerpartleme  29752  eulerpartlem1  29756  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemr  29763  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgs2  29769  eulerpartlemn  29770  fib0  29788  fib1  29789  fibp1  29790  knoppcnlem1  31653  knoppcnlem6  31658  poimirlem32  32611  heiborlem3  32782  eldiophb  36338  diophrw  36340  hbtlem1  36712  hbtlem7  36714  dgrsub2  36724  mpaaeu  36739  deg1mhm  36804  elrtrclrec  36992  brmptiunrelexpd  36994  brrtrclrec  37008  iunrelexp0  37013  iunrelexpmin2  37023  dfrtrcl3  37044  fvrtrcllb0d  37046  fvrtrcllb0da  37047  fvrtrcllb1d  37048  radcnvrat  37535  binomcxplemrat  37571  binomcxplemnotnn0  37577  expfac  38724  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  etransclem24  39151  etransclem25  39152  etransclem26  39153  etransclem28  39155  etransclem35  39162  etransclem37  39164  etransclem48  39175  fmtnoinf  39986  ply1mulgsum  41972