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

Theorem nnex 10642
Description: The set of positive integers 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 9645 . 2  |-  CC  e.  _V
2 nnsscn 10641 . 2  |-  NN  C_  CC
31, 2ssexi 4561 1  |-  NN  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1897   _Vcvv 3056   CCcc 9562   NNcn 10636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-i2m1 9632  ax-1ne0 9633  ax-rrecex 9636  ax-cnre 9637
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6317  df-om 6719  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-nn 10637
This theorem is referenced by:  dfnn2  10649  nn0ex  10903  rpnnen1lem1  11318  rpnnen1lem3  11320  rpnnen1lem4  11321  rpnnen1lem5  11322  nn0ennn  12223  facmapnn  12501  isercolllem2  13777  supcvg  13962  trireciplem  13968  expcnv  13970  geo2lim  13979  qnnen  14314  rpnnen2lem1  14315  rpnnen2lem2  14316  rpnnen  14327  rucALT  14330  prmex  14676  unbenlem  14900  vdwapfval  14969  vdwapf  14970  vdwlem6  14984  vdwlem7  14985  vdwlem8  14986  vdwlem11  14989  lcmsmapnnOLD  15059  prmormapnnOLD  15062  prmgaplcm  15079  prmgapprmo  15081  ndxarg  15189  odval  17228  odvalOLD  17231  gexval  17275  gexvalOLD  17277  ablfac1b  17751  pnrmopn  20407  1stcfb  20508  hausmapdom  20563  met1stc  21584  met2ndci  21585  rectbntr0  21898  metcld2  22324  elovolm  22476  elovolmr  22477  ovolmge0  22478  ovolgelb  22481  ovolctb  22491  ovol0  22494  ovolunlem1a  22497  ovolunlem1  22498  ovoliunlem1  22503  ovoliunlem2  22504  ovolshftlem2  22511  ovolicc2  22524  ioombl1  22563  mbfimaopnlem  22659  itg1climres  22720  mbfi1fseqlem6  22726  mbfi1flimlem  22728  mbfmullem2  22730  itg2monolem1  22756  itg2addlem  22764  plyeq0lem  23212  leibpi  23916  dfef2  23944  emcllem4  23972  emcllem6  23974  emcllem7  23975  lgamgulmlem6  24007  lgamcvg2  24028  basellem6  24060  basellem7  24061  basellem8  24062  basellem9  24063  vmaval  24088  sqff1o  24157  0sgmppw  24174  dchrisumlem3  24377  dirith2  24414  iseupa  25741  nmounbseqiALT  26467  nmobndseqiALT  26469  h2hcau  26680  h2hlm  26681  hcau  26885  hlimi  26889  hlimadd  26894  hhcms  26904  isch2  26924  chlimi  26935  hlim0  26936  hhsscms  26978  padct  28355  smatfval  28669  lmdvg  28807  esumfsup  28939  esumpcvgval  28947  esumcvg  28955  sigapildsys  29032  measiun  29088  voliune  29100  omssubadd  29176  omssubaddOLD  29180  carsggect  29198  carsgclctunlem2  29199  eulerpartlems  29241  eulerpartleme  29244  eulerpartlem1  29248  eulerpartlemb  29249  eulerpartlemt  29252  eulerpartgbij  29253  eulerpartlemr  29255  eulerpartlemmf  29256  eulerpartlemgvv  29257  eulerpartlemgf  29260  eulerpartlemgs2  29261  eulerpartlemn  29262  sinccvglem  30364  circum  30366  divcnvlin  30415  faclimlem2  30428  faclim2  30432  colinearex  30875  poimirlem32  32016  voliunnfl  32028  volsupnfl  32029  lmclim2  32131  geomcau  32132  rrncmslem  32208  eldioph3b  35651  lzenom  35656  diophin  35659  diophun  35660  pellexlem3  35719  pellexlem4  35720  pellexlem5  35721  eltrclrec  36316  brtrclrec  36332  iunrelexpmin1  36344  trclrelexplem  36347  dftrcl3  36356  fvtrcllb1d  36358  trclfvcom  36359  cnvtrclfv  36360  cotrcltrcl  36361  trclimalb2  36362  trclfvdecomr  36364  dfrtrcl4  36374  corcltrcl  36375  cotrclrcl  36378  hashnzfzclim  36714  dvradcnv2  36739  binomcxplemcvg  36746  binomcxplemdvsum  36747  binomcxplemnotnn0  36748  ssnnf1octb  37507  clim1fr1  37716  divcnvg  37744  wallispilem5  37968  wallispi  37969  stirlinglem1  37973  stirlinglem8  37980  stirlinglem14  37986  stirlinglem15  37987  fourierdlem103  38110  fourierdlem104  38111  fourierdlem112  38119  nnfoctbdjlem  38330  nnfoctbdj  38331  ismeannd  38342  caratheodorylem2  38385  isomenndlem  38388  hoicvrrex  38415  ovnsupge0  38416  ovnlecvr  38417  ovn0lem  38424  ovnsubaddlem1  38429  ovnsubadd  38431  sge0hsphoire  38448  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1lelem3  38452  hoidmv1le  38453  hoidmvlelem1  38454  hoidmvlelem2  38455  hoidmvlelem3  38456  hoidmvlelem4  38457  hoidmvlelem5  38458  hoidmvle  38459  ovnhoilem1  38460  ovnhoilem2  38461  ovnlecvr2  38469  hspmbllem2  38486  nnsgrpmgm  40088  nnsgrp  40089  nnsgrpnmnd  40090
  Copyright terms: Public domain W3C validator