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

Theorem nnex 10541
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 9572 . 2  |-  CC  e.  _V
2 nnsscn 10540 . 2  |-  NN  C_  CC
31, 2ssexi 4592 1  |-  NN  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   _Vcvv 3113   CCcc 9489   NNcn 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-cnex 9547  ax-resscn 9548  ax-1cn 9549  ax-icn 9550  ax-addcl 9551  ax-addrcl 9552  ax-mulcl 9553  ax-mulrcl 9554  ax-i2m1 9559  ax-1ne0 9560  ax-rrecex 9563  ax-cnre 9564
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-ov 6286  df-om 6680  df-recs 7042  df-rdg 7076  df-nn 10536
This theorem is referenced by:  dfnn2  10548  nn0ex  10800  nn0ennn  12056  isercolllem2  13450  supcvg  13629  trireciplem  13635  expcnv  13637  geo2lim  13646  xpnnenOLD  13803  qnnen  13807  rpnnen2lem1  13808  rpnnen2lem2  13809  rpnnen  13820  rucALT  13823  unbenlem  14284  vdwapfval  14347  vdwapf  14348  vdwlem6  14362  vdwlem7  14363  vdwlem8  14364  vdwlem11  14367  ndxarg  14509  odval  16361  gexval  16401  ablfac1b  16920  pnrmopn  19626  1stcfb  19728  hausmapdom  19783  met1stc  20775  met2ndci  20776  rectbntr0  21088  metcld2  21496  elovolm  21637  elovolmr  21638  ovolmge0  21639  ovolgelb  21642  ovolctb  21652  ovol0  21655  ovolunlem1a  21658  ovolunlem1  21659  ovoliunlem1  21664  ovoliunlem2  21665  ovolshftlem2  21672  ovolicc2  21684  ioombl1  21723  mbfimaopnlem  21813  itg1climres  21872  mbfi1fseqlem6  21878  mbfi1flimlem  21880  mbfmullem2  21882  itg2monolem1  21908  itg2addlem  21916  plyeq0lem  22358  leibpi  23017  dfef2  23044  emcllem4  23072  emcllem6  23074  emcllem7  23075  basellem6  23103  basellem7  23104  basellem8  23105  basellem9  23106  vmaval  23131  sqff1o  23200  0sgmppw  23217  dchrisumlem3  23420  dirith2  23457  iseupa  24657  nmounbseqiOLD  25385  nmobndseqiOLD  25387  h2hcau  25588  h2hlm  25589  hcau  25793  hlimi  25797  hlimadd  25802  hhcms  25812  isch2  25833  chlimi  25844  hlim0  25845  hhsscms  25887  lmdvg  27587  esumfsup  27732  esumpcvgval  27740  esumcvg  27748  measiun  27845  voliune  27857  eulerpartlems  27955  eulerpartleme  27958  eulerpartlem1  27962  eulerpartlemb  27963  eulerpartlemt  27966  eulerpartgbij  27967  eulerpartlemr  27969  eulerpartlemmf  27970  eulerpartlemgvv  27971  eulerpartlemgf  27974  eulerpartlemgs2  27975  eulerpartlemn  27976  lgamgulmlem6  28232  lgamcvg2  28253  sinccvglem  28529  circum  28531  divcnvlin  28611  faclimlem2  28762  faclim2  28766  colinearex  29303  voliunnfl  29651  volsupnfl  29652  lmclim2  29870  geomcau  29871  rrncmslem  29947  eldioph3b  30318  lzenom  30323  diophin  30326  diophun  30327  pellexlem3  30387  pellexlem4  30388  pellexlem5  30389  hashnzfzclim  30843  clim1fr1  31159  divcnvg  31185  wallispilem5  31385  wallispi  31386  stirlinglem1  31390  stirlinglem8  31397  stirlinglem14  31403  stirlinglem15  31404  fourierdlem103  31526  fourierdlem104  31527  fourierdlem112  31535
  Copyright terms: Public domain W3C validator