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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 8834 . 2  |-  CC  e.  _V
2 ax-resscn 8810 . 2  |-  RR  C_  CC
31, 2ssexi 4175 1  |-  RR  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   CCcc 8751   RRcr 8752
This theorem is referenced by:  xrex  10367  limsuple  11968  limsuplt  11969  limsupbnd1  11972  rlim  11985  rlimf  11991  rlimss  11992  ello12  12006  lo1f  12008  lo1dm  12009  elo12  12017  o1f  12019  o1dm  12020  o1of2  12102  o1rlimmul  12108  o1add2  12113  o1mul2  12114  o1sub2  12115  o1dif  12119  caucvgrlem  12161  fsumo1  12286  rpnnen  12521  cpnnen  12523  ruclem13  12536  ruc  12537  aleph1re  12539  aleph1irr  12540  cnfldds  16405  ismet  17904  tngngp2  18184  tngngpd  18185  tngngp  18186  tngnrg  18201  rerest  18326  xrtgioo  18328  xrrest  18329  xrsmopn  18334  opnreen  18352  rectbntr0  18353  xrge0tsms  18355  bcthlem1  18762  bcthlem5  18766  pmltpclem2  18825  ovolficcss  18845  ovolval  18849  elovolm  18850  elovolmr  18851  ovolmge0  18852  ovolgelb  18855  ovolctb2  18867  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliunlem2  18878  ovolshftlem2  18885  ovolicc2  18897  ismbl  18901  mblsplit  18907  voliunlem2  18924  voliunlem3  18925  ioombl1  18935  dyadmbl  18971  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbff  18998  ismbf  19001  ismbfcn  19002  mbfconst  19006  cncombf  19029  cnmbf  19030  0plef  19043  i1fd  19052  itg1ge0  19057  i1faddlem  19064  i1fmullem  19065  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  i1fmulclem  19073  i1fmulc  19074  itg1mulc  19075  i1fsub  19079  itg1sub  19080  itg1lea  19083  itg1le  19084  mbfi1fseqlem2  19087  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1flimlem  19093  mbfmullem2  19095  itg2val  19099  xrge0f  19102  itg2ge0  19106  itg2itg1  19107  itg20  19108  itg2le  19110  itg2const  19111  itg2const2  19112  itg2seq  19113  itg2uba  19114  itg2lea  19115  itg2mulclem  19117  itg2mulc  19118  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2i1fseq  19126  itg2addlem  19129  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  iblss  19175  i1fibl  19178  itgitg1  19179  itgle  19180  ibladdlem  19190  itgaddlem1  19193  iblabslem  19198  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2lem1  19202  bddmulibl  19209  dvf  19273  dvnfre  19317  dvmptcj  19333  dvmptre  19334  dvmptim  19335  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  c1liplem1  19359  c1lip2  19361  dvle  19370  dvivthlem1  19371  dvivth  19373  lhop2  19378  dvcnvrelem2  19381  dvcnvre  19382  dvfsumle  19384  dvfsumge  19385  dvfsumabs  19386  dvfsumlem2  19390  dvfsum2  19397  ftc2  19407  itgparts  19410  itgsubstlem  19411  aalioulem3  19730  taylthlem2  19769  taylth  19770  efcvx  19841  pige3  19901  dvrelog  20000  advlog  20017  advlogexp  20018  logccv  20026  dvcxp1  20098  loglesqr  20114  dmarea  20268  divsqrsumlem  20290  logexprlim  20480  vmadivsum  20647  rpvmasumlem  20652  mudivsum  20695  logdivsum  20698  log2sumbnd  20709  selberglem1  20710  selberglem2  20711  selberg2lem  20715  selberg2  20716  pntrsumo1  20730  selbergr  20733  raddcn  23317  xrge0tsmsd  23397  mbfmcnt  23588  isrrvv  23661  dstfrvclim1  23693  erdsze2lem1  23749  erdsze2lem2  23750  snmlval  23929  elee  24594  itg2addnclem  25003  itg2addnc  25005  itg2gt0cn  25006  ibladdnclem  25007  itgaddnclem1  25009  iblabsnclem  25014  iblabsnc  25015  iblmulc2nc  25016  itgmulc2nclem1  25017  bddiblnc  25021  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem3  25029  claddrvr  25751  rnegvex2  25764  negveudr  25772  subclrvd  25777  clsmulrv  25786  divclrvd  25798  intvlset  25801  filbcmb  26535  rrncmslem  26659  repwsmet  26661  rrnequiv  26662  ismrer1  26665  pell1qrval  27034  pell14qrval  27036  pell1234qrval  27038  lhe4.4ex1a  27649  addrval  27774  subrval  27775  mulvval  27776  climreeq  27842  dvcosre  27844  itgsin0pilem1  27847  itgsinexplem1  27851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-cnex 8809  ax-resscn 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator