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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 9073 . 2  |-  CC  e.  _V
2 ax-resscn 9049 . 2  |-  RR  C_  CC
31, 2ssexi 4350 1  |-  RR  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   _Vcvv 2958   CCcc 8990   RRcr 8991
This theorem is referenced by:  xrex  10611  limsuple  12274  limsuplt  12275  limsupbnd1  12278  rlim  12291  rlimf  12297  rlimss  12298  ello12  12312  lo1f  12314  lo1dm  12315  elo12  12323  o1f  12325  o1dm  12326  o1of2  12408  o1rlimmul  12414  o1add2  12419  o1mul2  12420  o1sub2  12421  o1dif  12425  caucvgrlem  12468  fsumo1  12593  rpnnen  12828  cpnnen  12830  ruclem13  12843  ruc  12844  aleph1re  12846  aleph1irr  12847  cnfldds  16715  ismet  18355  tngngp2  18695  tngngpd  18696  tngngp  18697  tngnrg  18712  rerest  18837  xrtgioo  18839  xrrest  18840  xrsmopn  18845  opnreen  18864  rectbntr0  18865  xrge0tsms  18867  bcthlem1  19279  bcthlem5  19283  pmltpclem2  19348  ovolficcss  19368  ovolval  19372  elovolm  19373  elovolmr  19374  ovolmge0  19375  ovolgelb  19378  ovolctb2  19390  ovolunlem1a  19394  ovolunlem1  19395  ovoliunlem1  19400  ovoliunlem2  19401  ovolshftlem2  19408  ovolicc2  19420  ismbl  19424  mblsplit  19430  voliunlem2  19447  voliunlem3  19448  ioombl1  19458  dyadmbl  19494  vitalilem2  19503  vitalilem3  19504  vitalilem4  19505  vitalilem5  19506  vitali  19507  mbff  19521  ismbf  19524  ismbfcn  19525  mbfconst  19529  cncombf  19552  cnmbf  19553  0plef  19566  i1fd  19575  itg1ge0  19580  i1faddlem  19587  i1fmullem  19588  i1fadd  19589  i1fmul  19590  itg1addlem4  19593  i1fmulclem  19596  i1fmulc  19597  itg1mulc  19598  i1fsub  19602  itg1sub  19603  itg1lea  19606  itg1le  19607  mbfi1fseqlem2  19610  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  mbfi1flimlem  19616  mbfmullem2  19618  itg2val  19622  xrge0f  19625  itg2ge0  19629  itg2itg1  19630  itg20  19631  itg2le  19633  itg2const  19634  itg2const2  19635  itg2seq  19636  itg2uba  19637  itg2lea  19638  itg2mulclem  19640  itg2mulc  19641  itg2splitlem  19642  itg2split  19643  itg2monolem1  19644  itg2mono  19647  itg2i1fseqle  19648  itg2i1fseq  19649  itg2addlem  19652  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  iblss  19698  i1fibl  19701  itgitg1  19702  itgle  19703  ibladdlem  19713  itgaddlem1  19716  iblabslem  19721  iblabs  19722  iblabsr  19723  iblmulc2  19724  itgmulc2lem1  19725  bddmulibl  19732  dvf  19796  dvnfre  19840  dvmptcj  19856  dvmptre  19857  dvmptim  19858  rolle  19876  cmvth  19877  mvth  19878  dvlip  19879  dvlipcn  19880  c1liplem1  19882  c1lip2  19884  dvle  19893  dvivthlem1  19894  dvivth  19896  lhop2  19901  dvcnvrelem2  19904  dvcnvre  19905  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem2  19913  dvfsum2  19920  ftc2  19930  itgparts  19933  itgsubstlem  19934  aalioulem3  20253  taylthlem2  20292  taylth  20293  efcvx  20367  pige3  20427  dvrelog  20530  advlog  20547  advlogexp  20548  logccv  20556  dvcxp1  20628  loglesqr  20644  dmarea  20798  divsqrsumlem  20820  logexprlim  21011  vmadivsum  21178  rpvmasumlem  21183  mudivsum  21226  logdivsum  21229  log2sumbnd  21240  selberglem1  21241  selberglem2  21242  selberg2lem  21246  selberg2  21247  pntrsumo1  21261  selbergr  21264  xrge0tsmsd  24225  replusg  24273  remulr  24274  rele2  24277  raddcn  24317  reust  24346  rrhcn  24382  rrhre  24389  dmvlsiga  24514  mbfmcnt  24620  sxbrsigalem0  24623  sxbrsigalem3  24624  dya2icoseg2  24630  sxbrsigalem2  24638  sitmcl  24665  isrrvv  24703  dstfrvclim1  24737  lgamgulmlem2  24816  erdsze2lem1  24891  erdsze2lem2  24892  snmlval  25020  elee  25835  mblfinlem3  26247  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  ibladdnclem  26263  itgaddnclem1  26265  iblabsnclem  26270  iblabsnc  26271  iblmulc2nc  26272  itgmulc2nclem1  26273  bddiblnc  26277  ftc1anclem3  26284  ftc1anclem4  26285  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  dvreasin  26292  dvreacos  26293  areacirclem1  26294  filbcmb  26444  rrncmslem  26543  repwsmet  26545  rrnequiv  26546  ismrer1  26549  pell1qrval  26911  pell14qrval  26913  pell1234qrval  26915  lhe4.4ex1a  27525  addrval  27649  subrval  27650  mulvval  27651  climreeq  27717  dvcosre  27719  itgsin0pilem1  27722  itgsinexplem1  27726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-cnex 9048  ax-resscn 9049
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator