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

Theorem nnex 10876
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
StepHypRef Expression
1 cnex 9874 . 2 ℂ ∈ V
2 nnsscn 10875 . 2 ℕ ⊆ ℂ
31, 2ssexi 4726 1 ℕ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Vcvv 3173  cc 9791  cn 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-i2m1 9861  ax-1ne0 9862  ax-rrecex 9865  ax-cnre 9866
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6936  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-nn 10871
This theorem is referenced by:  dfnn2  10883  nn0ex  11148  rpnnen1lem1OLD  11656  rpnnen1lem3OLD  11657  rpnnen1lem4OLD  11658  rpnnen1lem5OLD  11659  nn0ennn  12598  facmapnn  12892  isercolllem2  14193  supcvg  14376  trireciplem  14382  expcnv  14384  geo2lim  14394  qnnen  14730  rpnnen2lem1  14731  rpnnen2lem2  14732  rpnnen  14744  rucALT  14747  prmex  15178  unbenlem  15399  vdwapfval  15462  vdwapf  15463  vdwlem6  15477  vdwlem7  15478  vdwlem8  15479  vdwlem11  15482  prmgaplcm  15551  prmgapprmo  15553  ndxarg  15664  odval  17725  gexval  17765  ablfac1b  18241  pnrmopn  20905  1stcfb  21006  hausmapdom  21061  met1stc  22084  met2ndci  22085  rectbntr0  22391  metcld2  22858  elovolm  22995  elovolmr  22996  ovolmge0  22997  ovolgelb  23000  ovolctb  23010  ovol0  23013  ovolunlem1a  23016  ovolunlem1  23017  ovoliunlem1  23022  ovoliunlem2  23023  ovolshftlem2  23030  ovolicc2  23042  ioombl1  23082  mbfimaopnlem  23173  itg1climres  23232  mbfi1fseqlem6  23238  mbfi1flimlem  23240  mbfmullem2  23242  itg2monolem1  23268  itg2addlem  23276  plyeq0lem  23715  leibpi  24414  dfef2  24442  emcllem4  24470  emcllem6  24472  emcllem7  24473  lgamgulmlem6  24505  lgamcvg2  24526  basellem6  24557  basellem7  24558  basellem8  24559  basellem9  24560  vmaval  24584  sqff1o  24653  0sgmppw  24668  dchrisumlem3  24925  dirith2  24962  iseupa  26286  nmounbseqiALT  26811  nmobndseqiALT  26813  h2hcau  27014  h2hlm  27015  hcau  27219  hlimi  27223  hlimadd  27228  hhcms  27238  isch2  27258  chlimi  27269  hlim0  27270  hhsscms  27314  padct  28679  smatfval  28983  lmdvg  29121  esumfsup  29253  esumpcvgval  29261  esumcvg  29269  sigapildsys  29346  measiun  29402  voliune  29413  omssubadd  29483  carsggect  29501  carsgclctunlem2  29502  eulerpartlems  29543  eulerpartleme  29546  eulerpartlem1  29550  eulerpartlemb  29551  eulerpartlemt  29554  eulerpartgbij  29555  eulerpartlemr  29557  eulerpartlemmf  29558  eulerpartlemgvv  29559  eulerpartlemgf  29562  eulerpartlemgs2  29563  eulerpartlemn  29564  sinccvglem  30614  circum  30616  divcnvlin  30665  faclimlem2  30677  faclim2  30681  colinearex  31131  poimirlem32  32405  voliunnfl  32417  volsupnfl  32418  lmclim2  32518  geomcau  32519  rrncmslem  32595  eldioph3b  36140  lzenom  36145  diophin  36148  diophun  36149  pellexlem3  36207  pellexlem4  36208  pellexlem5  36209  eltrclrec  36785  brtrclrec  36801  iunrelexpmin1  36813  trclrelexplem  36816  dftrcl3  36825  fvtrcllb1d  36827  trclfvcom  36828  cnvtrclfv  36829  cotrcltrcl  36830  trclimalb2  36831  trclfvdecomr  36833  dfrtrcl4  36843  corcltrcl  36844  cotrclrcl  36847  hashnzfzclim  37337  dvradcnv2  37362  binomcxplemcvg  37369  binomcxplemdvsum  37370  binomcxplemnotnn0  37371  ssnnf1octb  38171  clim1fr1  38462  divcnvg  38488  wallispilem5  38756  wallispi  38757  stirlinglem1  38761  stirlinglem8  38768  stirlinglem14  38774  stirlinglem15  38775  fourierdlem103  38896  fourierdlem104  38897  fourierdlem112  38905  subsaliuncllem  39045  subsaliuncl  39046  nnfoctbdjlem  39142  nnfoctbdj  39143  ismeannd  39154  voliunsge0lem  39159  caratheodorylem2  39211  isomenndlem  39214  hoicvrrex  39240  ovnsupge0  39241  ovnlecvr  39242  ovn0lem  39249  ovnsubaddlem1  39254  ovnsubadd  39256  sge0hsphoire  39273  hoidmv1lelem1  39275  hoidmv1lelem2  39276  hoidmv1lelem3  39277  hoidmv1le  39278  hoidmvlelem1  39279  hoidmvlelem2  39280  hoidmvlelem3  39281  hoidmvlelem4  39282  hoidmvlelem5  39283  hoidmvle  39284  ovnhoilem1  39285  ovnhoilem2  39286  ovnlecvr2  39294  hspmbllem2  39311  ovolval2lem  39327  ovnsubadd2lem  39329  ovolval4lem2  39334  ovolval5lem1  39336  ovolval5lem2  39337  ovnovollem1  39340  ovnovollem2  39341  vonioolem1  39365  smflimlem6  39456  smfresal  39467  nnsgrpmgm  41598  nnsgrp  41599  nnsgrpnmnd  41600
  Copyright terms: Public domain W3C validator