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

Theorem reex 9632
Description: The real numbers form a set. See also reexALT 11298. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
reex  |-  RR  e.  _V

Proof of Theorem reex
StepHypRef Expression
1 cnex 9622 . 2  |-  CC  e.  _V
2 ax-resscn 9598 . 2  |-  RR  C_  CC
31, 2ssexi 4567 1  |-  RR  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869   _Vcvv 3082   CCcc 9539   RRcr 9540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-cnex 9597  ax-resscn 9598
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-in 3444  df-ss 3451
This theorem is referenced by:  reelprrecn  9633  negfi  10556  xrex  11301  limsuple  13529  limsupleOLD  13530  limsuplt  13531  limsupltOLD  13532  limsupbnd1  13537  limsupbnd1OLD  13538  rlim  13552  rlimf  13558  rlimss  13559  ello12  13573  lo1f  13575  lo1dm  13576  elo12  13584  o1f  13586  o1dm  13587  o1of2  13669  o1rlimmul  13675  o1add2  13680  o1mul2  13681  o1sub2  13682  o1dif  13686  caucvgrlem  13729  caucvgrlemOLD  13730  fsumo1  13865  rpnnen  14272  cpnnen  14274  ruclem13  14287  ruc  14288  aleph1re  14290  aleph1irr  14291  cnfldds  18973  replusg  19170  remulr  19171  rele2  19174  reds  19176  refldcj  19180  ismet  21330  tngngp2  21652  tngngpd  21653  tngngp  21654  tngnrg  21669  rerest  21814  xrtgioo  21816  xrrest  21817  xrsmopn  21822  opnreen  21841  rectbntr0  21842  xrge0tsms  21844  bcthlem1  22284  bcthlem5  22288  reust  22332  rrxip  22341  pmltpclem2  22392  ovolficcss  22414  ovolval  22418  ovolvalOLD  22419  elovolm  22420  elovolmr  22421  ovolmge0  22422  ovolgelb  22425  ovolctb2  22437  ovolunlem1a  22441  ovolunlem1  22442  ovoliunlem1  22447  ovoliunlem2  22448  ovolshftlem2  22455  ovolicc2  22468  ismbl  22472  mblsplit  22478  voliunlem3  22497  ioombl1  22507  dyadmbl  22550  vitalilem2  22559  vitalilem3  22560  vitalilem4  22561  vitalilem5  22562  vitali  22563  mbff  22575  ismbf  22578  ismbfcn  22579  mbfconst  22583  cncombf  22606  cnmbf  22607  0plef  22622  i1fd  22631  itg1ge0  22636  i1faddlem  22643  i1fmullem  22644  i1fadd  22645  i1fmul  22646  itg1addlem4  22649  i1fmulclem  22652  i1fmulc  22653  itg1mulc  22654  i1fsub  22658  itg1sub  22659  itg1lea  22662  itg1le  22663  mbfi1fseqlem2  22666  mbfi1fseqlem4  22668  mbfi1fseqlem5  22669  mbfi1flimlem  22672  mbfmullem2  22674  itg2val  22678  xrge0f  22681  itg2ge0  22685  itg2itg1  22686  itg20  22687  itg2le  22689  itg2const  22690  itg2const2  22691  itg2seq  22692  itg2uba  22693  itg2lea  22694  itg2mulclem  22696  itg2mulc  22697  itg2splitlem  22698  itg2split  22699  itg2monolem1  22700  itg2mono  22703  itg2i1fseqle  22704  itg2i1fseq  22705  itg2addlem  22708  itg2gt0  22710  itg2cnlem1  22711  itg2cnlem2  22712  iblss  22754  i1fibl  22757  itgitg1  22758  itgle  22759  ibladdlem  22769  itgaddlem1  22772  iblabslem  22777  iblabs  22778  iblabsr  22779  iblmulc2  22780  itgmulc2lem1  22781  bddmulibl  22788  dvnfre  22898  c1liplem1  22940  c1lip2  22942  lhop2  22959  dvcnvrelem2  22962  taylthlem2  23321  dmarea  23875  vmadivsum  24312  rpvmasumlem  24317  mudivsum  24360  selberglem1  24375  selberglem2  24376  selberg2lem  24380  selberg2  24381  pntrsumo1  24395  selbergr  24398  iscgrgd  24550  elee  24916  xrge0tsmsd  28550  nn0omnd  28606  xrge0slmod  28609  raddcn  28737  rrhcn  28803  qqtopn  28817  dmvlsiga  28953  ddeval1  29059  ddeval0  29060  ddemeas  29061  mbfmcnt  29092  sxbrsigalem0  29095  sxbrsigalem3  29096  sxbrsigalem2  29110  isrrvv  29278  dstfrvclim1  29312  signsplypnf  29441  erdsze2lem1  29928  erdsze2lem2  29929  snmlval  30056  icoreresf  31713  icoreval  31714  poimirlem29  31927  poimirlem30  31928  poimirlem31  31929  poimir  31931  broucube  31932  mblfinlem3  31937  itg2addnclem  31951  itg2addnclem3  31953  itg2addnc  31954  itg2gt0cn  31955  ibladdnclem  31956  itgaddnclem1  31958  iblabsnclem  31963  iblabsnc  31964  iblmulc2nc  31965  itgmulc2nclem1  31966  bddiblnc  31970  ftc1anclem3  31977  ftc1anclem4  31978  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  filbcmb  32025  rrncmslem  32122  repwsmet  32124  rrnequiv  32125  ismrer1  32128  pell1qrval  35656  pell14qrval  35658  pell1234qrval  35660  addrval  36721  subrval  36722  mulvval  36723  climreeq  37557  limsupre  37585  limsupreOLD  37586  limcresiooub  37587  limcresioolb  37588  icccncfext  37629  cncfiooicclem1  37635  itgsubsticclem  37716  dirkerval  37817  dirkercncflem4  37832  fourierdlem14  37847  fourierdlem15  37848  fourierdlem32  37866  fourierdlem33  37867  fourierdlem54  37888  fourierdlem62  37896  fourierdlem70  37904  fourierdlem81  37915  fourierdlem92  37926  fourierdlem102  37936  fourierdlem111  37945  fourierdlem114  37948  etransclem2  37965  hoicvr  38189  hoissrrn  38190  hoiprodcl2  38196  hoicvrrex  38197  ovn0lem  38206  ovn02  38209  refdivpm  39699  elbigo2  39707  elbigof  39709  elbigodm  39710  elbigoimp  39711  elbigolo1  39712
  Copyright terms: Public domain W3C validator