Theorem nn0ex 12448

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 12443	. 2 ⊢ ℕ0 = (ℕ ∪ {0})
2		nnex 12192	. . 3 ⊢ ℕ ∈ V
3		snex 5391	. . 3 ⊢ {0} ∈ V
4	2, 3	unex 7720	. 2 ⊢ (ℕ ∪ {0}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ ℕ0 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912  {csn 4589  0cc0 11068  ℕcn 12186  ℕ₀cn0 12442

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-1cn 11126  ax-addcl 11128

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 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  nn0ennn  13944  nnenom  13945  fsuppmapnn0fiub0  13958  suppssfz  13959  fsuppmapnn0ub  13960  mptnn0fsupp  13962  mptnn0fsuppr  13964  wrdexg  14489  elovmptnn0wrd  14524  rtrclreclem1  15023  dfrtrclrec2  15024  rtrclreclem2  15025  rtrclreclem4  15027  expcnv  15830  geolim  15836  cvgrat  15849  mertenslem2  15851  bpolylem  16014  eftlub  16077  bitsfval  16393  bitsf  16397  sadfval  16422  smufval  16447  smupf  16448  1arith  16898  ramcl  17000  smndex1ibas  18827  smndex1gbas  18829  smndex1gid  18830  smndex1igid  18831  smndex1mnd  18837  smndex1id  18838  smndex1n0mnd  18839  smndex2dbas  18841  smndex2dnrinv  18842  smndex2hbas  18843  smndex2dlinvh  18844  odfval  19462  fsfnn0gsumfsffz  19913  gsummptnn0fz  19916  nn0srg  21354  psrbag  21826  evlsgsumadd  21998  evlsgsummul  21999  mhpfval  22025  mhpmulcl  22036  coe1fval  22090  fvcoe1  22092  coe1fval3  22093  coe1f2  22094  coe1sfi  22098  coe1fsupp  22099  00ply1bas  22124  ply1plusgfvi  22126  coe1z  22149  coe1add  22150  coe1addfv  22151  coe1mul2lem1  22153  coe1mul2lem2  22154  coe1mul2  22155  coe1tm  22159  coe1sclmul  22168  coe1sclmulfv  22169  coe1sclmul2  22170  ply1coefsupp  22184  ply1coe  22185  gsumsmonply1  22194  gsummoncoe1  22195  evls1gsumadd  22211  evls1gsummul  22212  evl1gsummul  22247  evls1fpws  22256  pmatcollpw1  22663  pmatcollpw2lem  22664  pmatcollpw2  22665  pmatcollpw3lem  22670  pm2mpcl  22684  idpm2idmp  22688  mply1topmatcllem  22690  mply1topmatcl  22692  mp2pm2mplem2  22694  mp2pm2mplem5  22697  mp2pm2mp  22698  pm2mpghmlem2  22699  pm2mpghm  22703  pm2mpmhmlem2  22706  monmat2matmon  22711  pm2mp  22712  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cpmidpmatlem2  22758  cpmadumatpolylem1  22768  cpmadumatpolylem2  22769  chcoeffeqlem  22772  cayhamlem3  22774  cayhamlem4  22775  dyadmax  25499  cpnfval  25834  deg1ldg  25997  deg1leb  26000  deg1val  26001  deg1mul3  26021  deg1mul3le  26022  uc1pmon1p  26057  plyval  26098  elply2  26101  plyf  26103  elplyr  26106  plyeq0lem  26115  plyeq0  26116  plypf1  26117  plyaddlem1  26118  plyaddlem  26120  plymullem  26121  coeeulem  26129  coeeq  26132  dgrlem  26134  coeidlem  26142  coeaddlem  26154  coemulc  26160  coe0  26161  coesub  26162  dgradd2  26174  dgrcolem2  26180  plydivlem4  26204  plydiveu  26206  vieta1lem2  26219  taylfval  26266  pserval  26319  dvradcnv  26330  pserdvlem2  26338  abelthlem1  26341  abelthlem3  26343  abelthlem6  26346  logtayl  26569  leibpi  26852  sqff1o  27092  clwwlknonmpo  30018  ressply1evls1  33534  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  gsummoncoe1fzo  33563  ply1degltdimlem  33618  evls1fldgencl  33665  eulerpartleme  34354  eulerpartlem1  34358  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemr  34365  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgs2  34371  eulerpartlemn  34372  fib0  34390  fib1  34391  fibp1  34392  lpadval  34667  knoppcnlem1  36481  knoppcnlem6  36486  poimirlem32  37646  heiborlem3  37807  aks6d1c1  42104  aks6d1c2lem3  42114  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5lem2  42126  aks6d1c5  42127  sticksstones14  42148  sticksstones20  42154  sticksstones23  42157  aks6d1c6lem1  42158  aks6d1c6lem2  42159  eldiophb  42745  diophrw  42747  hbtlem1  43112  hbtlem7  43114  dgrsub2  43124  mpaaeu  43139  deg1mhm  43189  elrtrclrec  43670  brmptiunrelexpd  43672  brrtrclrec  43686  iunrelexp0  43691  iunrelexpmin2  43701  dfrtrcl3  43722  fvrtrcllb0d  43724  fvrtrcllb0da  43725  fvrtrcllb1d  43726  radcnvrat  44303  binomcxplemrat  44339  binomcxplemnotnn0  44345  expfac  45655  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  etransclem24  46256  etransclem25  46257  etransclem26  46258  etransclem28  46260  etransclem35  46267  etransclem37  46269  etransclem48  46280  fmtnoinf  47537  nn0mnd  48167  ply1mulgsum  48379  itcovalpclem1  48659  itcovalpclem2  48660  itcovalt2lem1  48664  itcovalt2lem2  48665  ackvalsuc1mpt  48667  ackval0  48669  ackendofnn0  48673  ackvalsucsucval  48677