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

Theorem nnex 10537
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 9562 . 2  |-  CC  e.  _V
2 nnsscn 10536 . 2  |-  NN  C_  CC
31, 2ssexi 4582 1  |-  NN  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   _Vcvv 3106   CCcc 9479   NNcn 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-om 6674  df-recs 7034  df-rdg 7068  df-nn 10532
This theorem is referenced by:  dfnn2  10544  nn0ex  10797  nn0ennn  12071  isercolllem2  13570  supcvg  13749  trireciplem  13755  expcnv  13757  geo2lim  13766  xpnnenOLD  14027  qnnen  14031  rpnnen2lem1  14032  rpnnen2lem2  14033  rpnnen  14044  rucALT  14047  unbenlem  14510  vdwapfval  14573  vdwapf  14574  vdwlem6  14588  vdwlem7  14589  vdwlem8  14590  vdwlem11  14593  ndxarg  14736  odval  16757  gexval  16797  ablfac1b  17316  pnrmopn  20011  1stcfb  20112  hausmapdom  20167  met1stc  21190  met2ndci  21191  rectbntr0  21503  metcld2  21911  elovolm  22052  elovolmr  22053  ovolmge0  22054  ovolgelb  22057  ovolctb  22067  ovol0  22070  ovolunlem1a  22073  ovolunlem1  22074  ovoliunlem1  22079  ovoliunlem2  22080  ovolshftlem2  22087  ovolicc2  22099  ioombl1  22138  mbfimaopnlem  22228  itg1climres  22287  mbfi1fseqlem6  22293  mbfi1flimlem  22295  mbfmullem2  22297  itg2monolem1  22323  itg2addlem  22331  plyeq0lem  22773  leibpi  23470  dfef2  23498  emcllem4  23526  emcllem6  23528  emcllem7  23529  basellem6  23557  basellem7  23558  basellem8  23559  basellem9  23560  vmaval  23585  sqff1o  23654  0sgmppw  23671  dchrisumlem3  23874  dirith2  23911  iseupa  25167  nmounbseqiALT  25891  nmobndseqiALT  25893  h2hcau  26094  h2hlm  26095  hcau  26299  hlimi  26303  hlimadd  26308  hhcms  26318  isch2  26339  chlimi  26350  hlim0  26351  hhsscms  26393  padct  27776  lmdvg  28170  esumfsup  28299  esumpcvgval  28307  esumcvg  28315  sigapildsys  28388  measiun  28426  voliune  28438  omssubadd  28508  carsggect  28526  carsgclctunlem2  28527  eulerpartlems  28563  eulerpartleme  28566  eulerpartlem1  28570  eulerpartlemb  28571  eulerpartlemt  28574  eulerpartgbij  28575  eulerpartlemr  28577  eulerpartlemmf  28578  eulerpartlemgvv  28579  eulerpartlemgf  28582  eulerpartlemgs2  28583  eulerpartlemn  28584  lgamgulmlem6  28840  lgamcvg2  28861  sinccvglem  29302  circum  29304  divcnvlin  29359  faclimlem2  29410  faclim2  29414  colinearex  29938  voliunnfl  30298  volsupnfl  30299  lmclim2  30491  geomcau  30492  rrncmslem  30568  eldioph3b  30937  lzenom  30942  diophin  30945  diophun  30946  pellexlem3  31006  pellexlem4  31007  pellexlem5  31008  hashnzfzclim  31468  dvradcnv2  31493  binomcxplemcvg  31500  binomcxplemdvsum  31501  binomcxplemnotnn0  31502  clim1fr1  31846  divcnvg  31872  wallispilem5  32090  wallispi  32091  stirlinglem1  32095  stirlinglem8  32102  stirlinglem14  32108  stirlinglem15  32109  fourierdlem103  32231  fourierdlem104  32232  fourierdlem112  32240  nnsgrpmgm  32876  nnsgrp  32877  nnsgrpnmnd  32878  iunrelexpmin1  38207  eltrclrec  38209  brtrclrec  38210  dftrcl3  38213  dfrtrcl4  38215  trclrelexplem  38229  corcltrcl  38231  cotrclrcl  38232  cotrcltrcl  38233
  Copyright terms: Public domain W3C validator