Theorem nnex 12171

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 11110	. 2 ⊢ ℂ ∈ V
2		nnsscn 12170	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5250	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ℂcc 11027  ℕcn 12165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12166

This theorem is referenced by:  dfnn2  12178  nn0ex  12434  nn0ennn  13932  facmapnn  14238  isercolllem2  15619  supcvg  15812  trireciplem  15818  expcnv  15820  geo2lim  15831  qnnen  16171  rpnnen2lem1  16172  rpnnen2lem2  16173  rpnnen  16185  rucALT  16188  prmex  16637  unbenlem  16870  vdwapfval  16933  vdwapf  16934  vdwlem6  16948  vdwlem7  16949  vdwlem8  16950  vdwlem11  16953  prmgaplcm  17022  prmgapprmo  17024  ndxarg  17157  ex-chn2  18595  odfval  19498  odval  19500  gexval  19544  pnrmopn  23326  1stcfb  23428  hausmapdom  23483  met1stc  24504  met2ndci  24505  rectbntr0  24816  metcld2  25292  elovolmlem  25459  ovolctb  25475  ovol0  25478  mbfimaopnlem  25640  itg1climres  25699  mbfi1fseqlem6  25705  mbfi1flimlem  25707  mbfmullem2  25709  itg2monolem1  25735  itg2addlem  25743  plyeq0lem  26193  leibpi  26924  dfef2  26952  emcllem4  26980  emcllem6  26982  emcllem7  26983  lgamgulmlem6  27015  lgamcvg2  27036  basellem6  27067  basellem7  27068  basellem8  27069  basellem9  27070  dchrisumlem3  27472  dirith2  27509  nmounbseqiALT  30867  nmobndseqiALT  30869  h2hcau  31068  h2hlm  31069  hcau  31273  hlimi  31277  hlimadd  31282  hhcms  31292  isch2  31312  chlimi  31323  hlim0  31324  hhsscms  31367  padct  32810  smatfval  33979  lmdvg  34137  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  sigapildsys  34346  measiun  34402  voliune  34413  omssubadd  34484  carsggect  34502  carsgclctunlem2  34503  eulerpartlems  34544  eulerpartleme  34547  eulerpartlem1  34551  eulerpartlemb  34552  eulerpartlemt  34555  eulerpartgbij  34556  eulerpartlemr  34558  eulerpartlemmf  34559  eulerpartlemgvv  34560  eulerpartlemgf  34563  eulerpartlemgs2  34564  eulerpartlemn  34565  reprval  34794  repr0  34795  reprsuc  34799  reprss  34801  reprinrn  34802  reprlt  34803  hashreprin  34804  reprinfz1  34806  reprpmtf1o  34810  reprdifc  34811  breprexplemb  34815  breprexpnat  34818  vtsval  34821  circlemethnat  34825  circlevma  34826  circlemethhgt  34827  sinccvglem  35900  circum  35902  divcnvlin  35961  faclimlem2  35972  faclim2  35976  colinearex  36288  bj-ndxarg  37435  poimirlem32  38019  voliunnfl  38031  volsupnfl  38032  lmclim2  38125  geomcau  38126  rrncmslem  38199  fisdomnn  42728  eldioph3b  43214  lzenom  43219  diophin  43221  diophun  43222  pellexlem3  43276  pellexlem4  43277  pellexlem5  43278  eltrclrec  44124  brtrclrec  44140  iunrelexpmin1  44152  trclrelexplem  44155  dftrcl3  44164  fvtrcllb1d  44166  trclfvcom  44167  cnvtrclfv  44168  cotrcltrcl  44169  trclimalb2  44170  trclfvdecomr  44172  dfrtrcl4  44182  corcltrcl  44183  cotrclrcl  44186  hashnzfzclim  44766  dvradcnv2  44791  binomcxplemcvg  44798  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  ssnnf1octb  45641  clim1fr1  46046  divcnvg  46072  limsup10ex  46216  liminf10ex  46217  wallispilem5  46512  wallispi  46513  stirlinglem1  46517  stirlinglem8  46524  stirlinglem14  46530  stirlinglem15  46531  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  subsaliuncllem  46800  subsaliuncl  46801  nnfoctbdjlem  46898  nnfoctbdj  46899  ismeannd  46910  voliunsge0lem  46915  caratheodorylem2  46970  isomenndlem  46973  hoicvrrex  46999  ovnsupge0  47000  ovnlecvr  47001  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  sge0hsphoire  47032  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvlelem5  47042  hoidmvle  47043  ovnhoilem1  47044  ovnhoilem2  47045  ovnlecvr2  47053  hspmbllem2  47070  ovolval2lem  47086  ovnsubadd2lem  47088  ovolval4lem2  47093  ovolval5lem1  47095  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  vonioolem1  47123  smflimlem6  47219  smfresal  47231  fsupdm  47285  smfsupdmmbllem  47287  finfdm  47289  smfinfdmmbllem  47291  nthrucw  47331  nnsgrpmgm  48667  nnsgrp  48668  nnsgrpnmnd  48669