MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnex Unicode version

Theorem nnex 9970
Description: The set of natural numbers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
nnex  |-  NN  e.  _V

Proof of Theorem nnex
StepHypRef Expression
1 cnex 9035 . 2  |-  CC  e.  _V
2 nnsscn 9969 . 2  |-  NN  C_  CC
31, 2ssexi 4316 1  |-  NN  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2924   CCcc 8952   NNcn 9964
This theorem is referenced by:  dfnn2  9977  nn0ex  10191  nn0ennn  11281  isercolllem2  12422  supcvg  12598  trireciplem  12604  expcnv  12606  geo2lim  12615  xpnnenOLD  12772  qnnen  12776  rpnnen2lem1  12777  rpnnen2lem2  12778  rpnnen  12789  rucALT  12792  unbenlem  13239  vdwapfval  13302  vdwapf  13303  vdwlem6  13317  vdwlem7  13318  vdwlem8  13319  vdwlem11  13322  ndxarg  13452  odval  15135  odf  15138  gexval  15175  ablfac1b  15591  pnrmopn  17369  1stcfb  17469  hausmapdom  17524  met1stc  18512  met2ndci  18513  rectbntr0  18824  metcld2  19220  elovolm  19332  elovolmr  19333  ovolmge0  19334  ovolgelb  19337  ovolctb  19347  ovol0  19350  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovolshftlem2  19367  ovolicc2  19379  ioombl1  19417  mbfimaopnlem  19508  itg1climres  19567  mbfi1fseqlem6  19573  mbfi1flimlem  19575  mbfmullem2  19577  itg2monolem1  19603  itg2addlem  19611  plyeq0lem  20090  leibpi  20743  dfef2  20770  emcllem4  20798  emcllem6  20800  emcllem7  20801  basellem6  20829  basellem7  20830  basellem8  20831  basellem9  20832  vmaval  20857  vmaf  20863  sqff1o  20926  0sgmppw  20943  dchrisumlem3  21146  dirith2  21183  iseupa  21648  nmounbseqiOLD  22240  nmobndseqiOLD  22242  h2hcau  22443  h2hlm  22444  hcau  22647  hlimi  22651  hlimadd  22656  hhcms  22666  isch2  22687  chlimi  22698  hlim0  22699  hhsscms  22740  lmdvg  24299  esumfsup  24421  esumpcvgval  24429  esumcvg  24437  measiun  24533  voliune  24546  lgamgulmlem6  24779  lgamcvg2  24800  sinccvglem  25070  circum  25072  divcnvlin  25173  faclimlem2  25319  faclim2  25323  colinearex  25906  voliunnfl  26157  volsupnfl  26158  lmclim2  26362  geomcau  26363  rrncmslem  26439  eldioph3b  26721  lzenom  26726  diophin  26729  diophun  26730  pellexlem3  26792  pellexlem4  26793  pellexlem5  26794  clim1fr1  27602  wallispilem5  27693  wallispi  27694  stirlinglem1  27698  stirlinglem8  27705  stirlinglem14  27711  stirlinglem15  27712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-i2m1 9022  ax-1ne0 9023  ax-rrecex 9026  ax-cnre 9027
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-recs 6600  df-rdg 6635  df-nn 9965
  Copyright terms: Public domain W3C validator