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

Theorem nnex 12167
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 11140 . 2 ℂ ∈ V
2 nnsscn 12166 . 2 ℕ ⊆ ℂ
31, 2ssexi 5283 1 ℕ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3447  cc 11057  cn 12161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-1cn 11117  ax-addcl 11119
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-om 7807  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-nn 12162
This theorem is referenced by:  dfnn2  12174  nn0ex  12427  nn0ennn  13893  facmapnn  14194  isercolllem2  15559  supcvg  15749  trireciplem  15755  expcnv  15757  geo2lim  15768  qnnen  16103  rpnnen2lem1  16104  rpnnen2lem2  16105  rpnnen  16117  rucALT  16120  prmex  16561  unbenlem  16788  vdwapfval  16851  vdwapf  16852  vdwlem6  16866  vdwlem7  16867  vdwlem8  16868  vdwlem11  16871  prmgaplcm  16940  prmgapprmo  16942  ndxarg  17076  odfval  19322  odval  19324  gexval  19368  pnrmopn  22717  1stcfb  22819  hausmapdom  22874  met1stc  23900  met2ndci  23901  rectbntr0  24218  metcld2  24694  elovolmlem  24861  ovolctb  24877  ovol0  24880  mbfimaopnlem  25042  itg1climres  25102  mbfi1fseqlem6  25108  mbfi1flimlem  25110  mbfmullem2  25112  itg2monolem1  25138  itg2addlem  25146  plyeq0lem  25594  leibpi  26315  dfef2  26343  emcllem4  26371  emcllem6  26373  emcllem7  26374  lgamgulmlem6  26406  lgamcvg2  26427  basellem6  26458  basellem7  26459  basellem8  26460  basellem9  26461  dchrisumlem3  26862  dirith2  26899  nmounbseqiALT  29769  nmobndseqiALT  29771  h2hcau  29970  h2hlm  29971  hcau  30175  hlimi  30179  hlimadd  30184  hhcms  30194  isch2  30214  chlimi  30225  hlim0  30226  hhsscms  30269  padct  31690  smatfval  32440  lmdvg  32598  esumfsup  32733  esumpcvgval  32741  esumcvg  32749  sigapildsys  32825  measiun  32881  voliune  32892  omssubadd  32964  carsggect  32982  carsgclctunlem2  32983  eulerpartlems  33024  eulerpartleme  33027  eulerpartlem1  33031  eulerpartlemb  33032  eulerpartlemt  33035  eulerpartgbij  33036  eulerpartlemr  33038  eulerpartlemmf  33039  eulerpartlemgvv  33040  eulerpartlemgf  33043  eulerpartlemgs2  33044  eulerpartlemn  33045  reprval  33287  repr0  33288  reprsuc  33292  reprss  33294  reprinrn  33295  reprlt  33296  hashreprin  33297  reprinfz1  33299  reprpmtf1o  33303  reprdifc  33304  breprexplemb  33308  breprexpnat  33311  vtsval  33314  circlemethnat  33318  circlevma  33319  circlemethhgt  33320  sinccvglem  34324  circum  34326  divcnvlin  34368  faclimlem2  34380  faclim2  34384  colinearex  34698  bj-ndxarg  35598  poimirlem32  36160  voliunnfl  36172  volsupnfl  36173  lmclim2  36267  geomcau  36268  rrncmslem  36341  eldioph3b  41135  lzenom  41140  diophin  41142  diophun  41143  pellexlem3  41201  pellexlem4  41202  pellexlem5  41203  eltrclrec  42044  brtrclrec  42060  iunrelexpmin1  42072  trclrelexplem  42075  dftrcl3  42084  fvtrcllb1d  42086  trclfvcom  42087  cnvtrclfv  42088  cotrcltrcl  42089  trclimalb2  42090  trclfvdecomr  42092  dfrtrcl4  42102  corcltrcl  42103  cotrclrcl  42106  hashnzfzclim  42694  dvradcnv2  42719  binomcxplemcvg  42726  binomcxplemdvsum  42727  binomcxplemnotnn0  42728  ssnnf1octb  43506  clim1fr1  43932  divcnvg  43958  limsup10ex  44104  liminf10ex  44105  wallispilem5  44400  wallispi  44401  stirlinglem1  44405  stirlinglem8  44412  stirlinglem14  44418  stirlinglem15  44419  fourierdlem103  44540  fourierdlem104  44541  fourierdlem112  44549  subsaliuncllem  44688  subsaliuncl  44689  nnfoctbdjlem  44786  nnfoctbdj  44787  ismeannd  44798  voliunsge0lem  44803  caratheodorylem2  44858  isomenndlem  44861  hoicvrrex  44887  ovnsupge0  44888  ovnlecvr  44889  ovn0lem  44896  ovnsubaddlem1  44901  ovnsubadd  44903  sge0hsphoire  44920  hoidmv1lelem1  44922  hoidmv1lelem2  44923  hoidmv1lelem3  44924  hoidmv1le  44925  hoidmvlelem1  44926  hoidmvlelem2  44927  hoidmvlelem3  44928  hoidmvlelem4  44929  hoidmvlelem5  44930  hoidmvle  44931  ovnhoilem1  44932  ovnhoilem2  44933  ovnlecvr2  44941  hspmbllem2  44958  ovolval2lem  44974  ovnsubadd2lem  44976  ovolval4lem2  44981  ovolval5lem1  44983  ovolval5lem2  44984  ovnovollem1  44987  ovnovollem2  44988  vonioolem1  45011  smflimlem6  45107  smfresal  45119  fsupdm  45173  smfsupdmmbllem  45175  finfdm  45177  smfinfdmmbllem  45179  nnsgrpmgm  46200  nnsgrp  46201  nnsgrpnmnd  46202
  Copyright terms: Public domain W3C validator