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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 8818 . 2  |-  CC  e.  _V
2 ax-resscn 8794 . 2  |-  RR  C_  CC
31, 2ssexi 4159 1  |-  RR  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   CCcc 8735   RRcr 8736
This theorem is referenced by:  xrex  10351  limsuple  11952  limsuplt  11953  limsupbnd1  11956  rlim  11969  rlimf  11975  rlimss  11976  ello12  11990  lo1f  11992  lo1dm  11993  elo12  12001  o1f  12003  o1dm  12004  o1of2  12086  o1rlimmul  12092  o1add2  12097  o1mul2  12098  o1sub2  12099  o1dif  12103  caucvgrlem  12145  fsumo1  12270  rpnnen  12505  cpnnen  12507  ruclem13  12520  ruc  12521  aleph1re  12523  aleph1irr  12524  cnfldds  16389  ismet  17888  tngngp2  18168  tngngpd  18169  tngngp  18170  tngnrg  18185  rerest  18310  xrtgioo  18312  xrrest  18313  xrsmopn  18318  opnreen  18336  rectbntr0  18337  xrge0tsms  18339  bcthlem1  18746  bcthlem5  18750  pmltpclem2  18809  ovolficcss  18829  ovolval  18833  elovolm  18834  elovolmr  18835  ovolmge0  18836  ovolgelb  18839  ovolctb2  18851  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovolshftlem2  18869  ovolicc2  18881  ismbl  18885  mblsplit  18891  voliunlem2  18908  voliunlem3  18909  ioombl1  18919  dyadmbl  18955  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbff  18982  ismbf  18985  ismbfcn  18986  mbfconst  18990  cncombf  19013  cnmbf  19014  0plef  19027  i1fd  19036  itg1ge0  19041  i1faddlem  19048  i1fmullem  19049  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulclem  19057  i1fmulc  19058  itg1mulc  19059  i1fsub  19063  itg1sub  19064  itg1lea  19067  itg1le  19068  mbfi1fseqlem2  19071  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flimlem  19077  mbfmullem2  19079  itg2val  19083  xrge0f  19086  itg2ge0  19090  itg2itg1  19091  itg20  19092  itg2le  19094  itg2const  19095  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2lea  19099  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2i1fseq  19110  itg2addlem  19113  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  iblss  19159  i1fibl  19162  itgitg1  19163  itgle  19164  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  dvf  19257  dvnfre  19301  dvmptcj  19317  dvmptre  19318  dvmptim  19319  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  c1liplem1  19343  c1lip2  19345  dvle  19354  dvivthlem1  19355  dvivth  19357  lhop2  19362  dvcnvrelem2  19365  dvcnvre  19366  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsum2  19381  ftc2  19391  itgparts  19394  itgsubstlem  19395  aalioulem3  19714  taylthlem2  19753  taylth  19754  efcvx  19825  pige3  19885  dvrelog  19984  advlog  20001  advlogexp  20002  logccv  20010  dvcxp1  20082  loglesqr  20098  dmarea  20252  divsqrsumlem  20274  logexprlim  20464  vmadivsum  20631  rpvmasumlem  20636  mudivsum  20679  logdivsum  20682  log2sumbnd  20693  selberglem1  20694  selberglem2  20695  selberg2lem  20699  selberg2  20700  pntrsumo1  20714  selbergr  20717  raddcn  23302  xrge0tsmsd  23382  mbfmcnt  23573  isrrvv  23646  dstfrvclim1  23678  erdsze2lem1  23734  erdsze2lem2  23735  snmlval  23914  elee  24522  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem3  24926  claddrvr  25648  rnegvex2  25661  negveudr  25669  subclrvd  25674  clsmulrv  25683  divclrvd  25695  intvlset  25698  filbcmb  26432  rrncmslem  26556  repwsmet  26558  rrnequiv  26559  ismrer1  26562  pell1qrval  26931  pell14qrval  26933  pell1234qrval  26935  lhe4.4ex1a  27546  addrval  27671  subrval  27672  mulvval  27673  climreeq  27739  dvcosre  27741  itgsin0pilem1  27744  itgsinexplem1  27748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-cnex 8793  ax-resscn 8794
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator