Theorem nnex 12180

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 11119	. 2 ⊢ ℂ ∈ V
2		nnsscn 12179	. 2 ⊢ ℕ ⊆ ℂ
3	1, 2	ssexi 5263	1 ⊢ ℕ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  ℕcn 12174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175

This theorem is referenced by:  dfnn2  12187  nn0ex  12443  nn0ennn  13941  facmapnn  14247  isercolllem2  15628  supcvg  15821  trireciplem  15827  expcnv  15829  geo2lim  15840  qnnen  16180  rpnnen2lem1  16181  rpnnen2lem2  16182  rpnnen  16194  rucALT  16197  prmex  16646  unbenlem  16879  vdwapfval  16942  vdwapf  16943  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  vdwlem11  16962  prmgaplcm  17031  prmgapprmo  17033  ndxarg  17166  ex-chn2  18604  odfval  19507  odval  19509  gexval  19553  pnrmopn  23308  1stcfb  23410  hausmapdom  23465  met1stc  24486  met2ndci  24487  rectbntr0  24798  metcld2  25274  elovolmlem  25441  ovolctb  25457  ovol0  25460  mbfimaopnlem  25622  itg1climres  25681  mbfi1fseqlem6  25687  mbfi1flimlem  25689  mbfmullem2  25691  itg2monolem1  25717  itg2addlem  25725  plyeq0lem  26175  leibpi  26906  dfef2  26934  emcllem4  26962  emcllem6  26964  emcllem7  26965  lgamgulmlem6  26997  lgamcvg2  27018  basellem6  27049  basellem7  27050  basellem8  27051  basellem9  27052  dchrisumlem3  27454  dirith2  27491  nmounbseqiALT  30849  nmobndseqiALT  30851  h2hcau  31050  h2hlm  31051  hcau  31255  hlimi  31259  hlimadd  31264  hhcms  31274  isch2  31294  chlimi  31305  hlim0  31306  hhsscms  31349  padct  32791  smatfval  33939  lmdvg  34097  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  sigapildsys  34306  measiun  34362  voliune  34373  omssubadd  34444  carsggect  34462  carsgclctunlem2  34463  eulerpartlems  34504  eulerpartleme  34507  eulerpartlem1  34511  eulerpartlemb  34512  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemr  34518  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgf  34523  eulerpartlemgs2  34524  eulerpartlemn  34525  reprval  34754  repr0  34755  reprsuc  34759  reprss  34761  reprinrn  34762  reprlt  34763  hashreprin  34764  reprinfz1  34766  reprpmtf1o  34770  reprdifc  34771  breprexplemb  34775  breprexpnat  34778  vtsval  34781  circlemethnat  34785  circlevma  34786  circlemethhgt  34787  sinccvglem  35854  circum  35856  divcnvlin  35915  faclimlem2  35926  faclim2  35930  colinearex  36242  bj-ndxarg  37389  poimirlem32  37973  voliunnfl  37985  volsupnfl  37986  lmclim2  38079  geomcau  38080  rrncmslem  38153  fisdomnn  42683  eldioph3b  43197  lzenom  43202  diophin  43204  diophun  43205  pellexlem3  43259  pellexlem4  43260  pellexlem5  43261  eltrclrec  44107  brtrclrec  44123  iunrelexpmin1  44135  trclrelexplem  44138  dftrcl3  44147  fvtrcllb1d  44149  trclfvcom  44150  cnvtrclfv  44151  cotrcltrcl  44152  trclimalb2  44153  trclfvdecomr  44155  dfrtrcl4  44165  corcltrcl  44166  cotrclrcl  44169  hashnzfzclim  44749  dvradcnv2  44774  binomcxplemcvg  44781  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  ssnnf1octb  45624  clim1fr1  46031  divcnvg  46057  limsup10ex  46201  liminf10ex  46202  wallispilem5  46497  wallispi  46498  stirlinglem1  46502  stirlinglem8  46509  stirlinglem14  46515  stirlinglem15  46516  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  subsaliuncllem  46785  subsaliuncl  46786  nnfoctbdjlem  46883  nnfoctbdj  46884  ismeannd  46895  voliunsge0lem  46900  caratheodorylem2  46955  isomenndlem  46958  hoicvrrex  46984  ovnsupge0  46985  ovnlecvr  46986  ovn0lem  46993  ovnsubaddlem1  46998  ovnsubadd  47000  sge0hsphoire  47017  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  hspmbllem2  47055  ovolval2lem  47071  ovnsubadd2lem  47073  ovolval4lem2  47078  ovolval5lem1  47080  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  vonioolem1  47108  smflimlem6  47204  smfresal  47216  fsupdm  47270  smfsupdmmbllem  47272  finfdm  47274  smfinfdmmbllem  47276  nthrucw  47316  nnsgrpmgm  48652  nnsgrp  48653  nnsgrpnmnd  48654