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

Theorem nnex 10548
Description: The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
nnex  |-  NN  e.  _V

Proof of Theorem nnex
StepHypRef Expression
1 cnex 9576 . 2  |-  CC  e.  _V
2 nnsscn 10547 . 2  |-  NN  C_  CC
31, 2ssexi 4582 1  |-  NN  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   _Vcvv 3095   CCcc 9493   NNcn 10542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10543
This theorem is referenced by:  dfnn2  10555  nn0ex  10807  nn0ennn  12068  isercolllem2  13467  supcvg  13646  trireciplem  13652  expcnv  13654  geo2lim  13663  xpnnenOLD  13820  qnnen  13824  rpnnen2lem1  13825  rpnnen2lem2  13826  rpnnen  13837  rucALT  13840  unbenlem  14303  vdwapfval  14366  vdwapf  14367  vdwlem6  14381  vdwlem7  14382  vdwlem8  14383  vdwlem11  14386  ndxarg  14529  odval  16432  gexval  16472  ablfac1b  16995  pnrmopn  19717  1stcfb  19819  hausmapdom  19874  met1stc  20897  met2ndci  20898  rectbntr0  21210  metcld2  21618  elovolm  21759  elovolmr  21760  ovolmge0  21761  ovolgelb  21764  ovolctb  21774  ovol0  21777  ovolunlem1a  21780  ovolunlem1  21781  ovoliunlem1  21786  ovoliunlem2  21787  ovolshftlem2  21794  ovolicc2  21806  ioombl1  21845  mbfimaopnlem  21935  itg1climres  21994  mbfi1fseqlem6  22000  mbfi1flimlem  22002  mbfmullem2  22004  itg2monolem1  22030  itg2addlem  22038  plyeq0lem  22480  leibpi  23145  dfef2  23172  emcllem4  23200  emcllem6  23202  emcllem7  23203  basellem6  23231  basellem7  23232  basellem8  23233  basellem9  23234  vmaval  23259  sqff1o  23328  0sgmppw  23345  dchrisumlem3  23548  dirith2  23585  iseupa  24837  nmounbseqiOLD  25565  nmobndseqiOLD  25567  h2hcau  25768  h2hlm  25769  hcau  25973  hlimi  25977  hlimadd  25982  hhcms  25992  isch2  26013  chlimi  26024  hlim0  26025  hhsscms  26067  lmdvg  27808  esumfsup  27949  esumpcvgval  27957  esumcvg  27965  measiun  28062  voliune  28074  eulerpartlems  28172  eulerpartleme  28175  eulerpartlem1  28179  eulerpartlemb  28180  eulerpartlemt  28183  eulerpartgbij  28184  eulerpartlemr  28186  eulerpartlemmf  28187  eulerpartlemgvv  28188  eulerpartlemgf  28191  eulerpartlemgs2  28192  eulerpartlemn  28193  lgamgulmlem6  28449  lgamcvg2  28470  sinccvglem  28911  circum  28913  divcnvlin  28993  faclimlem2  29144  faclim2  29148  colinearex  29685  voliunnfl  30033  volsupnfl  30034  lmclim2  30226  geomcau  30227  rrncmslem  30303  eldioph3b  30673  lzenom  30678  diophin  30681  diophun  30682  pellexlem3  30742  pellexlem4  30743  pellexlem5  30744  hashnzfzclim  31203  clim1fr1  31515  divcnvg  31541  wallispilem5  31740  wallispi  31741  stirlinglem1  31745  stirlinglem8  31752  stirlinglem14  31758  stirlinglem15  31759  fourierdlem103  31881  fourierdlem104  31882  fourierdlem112  31890  nnsgrpmgm  32341  nnsgrp  32342  nnsgrpnmnd  32343
  Copyright terms: Public domain W3C validator