Theorem nnex 11909

Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
nnex	⊢ ℕ ∈ V

Proof of Theorem nnex

Step	Hyp	Ref	Expression
1		cnex 10883	. 2 ⊢ ℂ ∈ V
2		nnsscn 11908	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5241	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904

This theorem is referenced by:  dfnn2  11916  nn0ex  12169  nn0ennn  13627  facmapnn  13927  isercolllem2  15305  supcvg  15496  trireciplem  15502  expcnv  15504  geo2lim  15515  qnnen  15850  rpnnen2lem1  15851  rpnnen2lem2  15852  rpnnen  15864  rucALT  15867  prmex  16310  unbenlem  16537  vdwapfval  16600  vdwapf  16601  vdwlem6  16615  vdwlem7  16616  vdwlem8  16617  vdwlem11  16620  prmgaplcm  16689  prmgapprmo  16691  ndxarg  16825  odfval  19055  odval  19057  gexval  19098  pnrmopn  22402  1stcfb  22504  hausmapdom  22559  met1stc  23583  met2ndci  23584  rectbntr0  23901  metcld2  24376  elovolmlem  24543  ovolctb  24559  ovol0  24562  mbfimaopnlem  24724  itg1climres  24784  mbfi1fseqlem6  24790  mbfi1flimlem  24792  mbfmullem2  24794  itg2monolem1  24820  itg2addlem  24828  plyeq0lem  25276  leibpi  25997  dfef2  26025  emcllem4  26053  emcllem6  26055  emcllem7  26056  lgamgulmlem6  26088  lgamcvg2  26109  basellem6  26140  basellem7  26141  basellem8  26142  basellem9  26143  dchrisumlem3  26544  dirith2  26581  nmounbseqiALT  29041  nmobndseqiALT  29043  h2hcau  29242  h2hlm  29243  hcau  29447  hlimi  29451  hlimadd  29456  hhcms  29466  isch2  29486  chlimi  29497  hlim0  29498  hhsscms  29541  padct  30956  smatfval  31647  lmdvg  31805  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  sigapildsys  32030  measiun  32086  voliune  32097  omssubadd  32167  carsggect  32185  carsgclctunlem2  32186  eulerpartlems  32227  eulerpartleme  32230  eulerpartlem1  32234  eulerpartlemb  32235  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemr  32241  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  reprval  32490  repr0  32491  reprsuc  32495  reprss  32497  reprinrn  32498  reprlt  32499  hashreprin  32500  reprinfz1  32502  reprpmtf1o  32506  reprdifc  32507  breprexplemb  32511  breprexpnat  32514  vtsval  32517  circlemethnat  32521  circlevma  32522  circlemethhgt  32523  sinccvglem  33530  circum  33532  divcnvlin  33604  faclimlem2  33616  faclim2  33620  colinearex  34289  bj-ndxarg  35175  poimirlem32  35736  voliunnfl  35748  volsupnfl  35749  lmclim2  35843  geomcau  35844  rrncmslem  35917  eldioph3b  40503  lzenom  40508  diophin  40510  diophun  40511  pellexlem3  40569  pellexlem4  40570  pellexlem5  40571  eltrclrec  41177  brtrclrec  41193  iunrelexpmin1  41205  trclrelexplem  41208  dftrcl3  41217  fvtrcllb1d  41219  trclfvcom  41220  cnvtrclfv  41221  cotrcltrcl  41222  trclimalb2  41223  trclfvdecomr  41225  dfrtrcl4  41235  corcltrcl  41236  cotrclrcl  41239  hashnzfzclim  41829  dvradcnv2  41854  binomcxplemcvg  41861  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  ssnnf1octb  42622  clim1fr1  43032  divcnvg  43058  limsup10ex  43204  liminf10ex  43205  wallispilem5  43500  wallispi  43501  stirlinglem1  43505  stirlinglem8  43512  stirlinglem14  43518  stirlinglem15  43519  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  subsaliuncllem  43786  subsaliuncl  43787  nnfoctbdjlem  43883  nnfoctbdj  43884  ismeannd  43895  voliunsge0lem  43900  caratheodorylem2  43955  isomenndlem  43958  hoicvrrex  43984  ovnsupge0  43985  ovnlecvr  43986  ovn0lem  43993  ovnsubaddlem1  43998  ovnsubadd  44000  sge0hsphoire  44017  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hoidmvle  44028  ovnhoilem1  44029  ovnhoilem2  44030  ovnlecvr2  44038  hspmbllem2  44055  ovolval2lem  44071  ovnsubadd2lem  44073  ovolval4lem2  44078  ovolval5lem1  44080  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  vonioolem1  44108  smflimlem6  44198  smfresal  44209  nnsgrpmgm  45258  nnsgrp  45259  nnsgrpnmnd  45260