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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 9071 . 2  |-  CC  e.  _V
2 ax-resscn 9047 . 2  |-  RR  C_  CC
31, 2ssexi 4348 1  |-  RR  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2956   CCcc 8988   RRcr 8989
This theorem is referenced by:  xrex  10609  limsuple  12272  limsuplt  12273  limsupbnd1  12276  rlim  12289  rlimf  12295  rlimss  12296  ello12  12310  lo1f  12312  lo1dm  12313  elo12  12321  o1f  12323  o1dm  12324  o1of2  12406  o1rlimmul  12412  o1add2  12417  o1mul2  12418  o1sub2  12419  o1dif  12423  caucvgrlem  12466  fsumo1  12591  rpnnen  12826  cpnnen  12828  ruclem13  12841  ruc  12842  aleph1re  12844  aleph1irr  12845  cnfldds  16713  ismet  18353  tngngp2  18693  tngngpd  18694  tngngp  18695  tngnrg  18710  rerest  18835  xrtgioo  18837  xrrest  18838  xrsmopn  18843  opnreen  18862  rectbntr0  18863  xrge0tsms  18865  bcthlem1  19277  bcthlem5  19281  pmltpclem2  19346  ovolficcss  19366  ovolval  19370  elovolm  19371  elovolmr  19372  ovolmge0  19373  ovolgelb  19376  ovolctb2  19388  ovolunlem1a  19392  ovolunlem1  19393  ovoliunlem1  19398  ovoliunlem2  19399  ovolshftlem2  19406  ovolicc2  19418  ismbl  19422  mblsplit  19428  voliunlem2  19445  voliunlem3  19446  ioombl1  19456  dyadmbl  19492  vitalilem2  19501  vitalilem3  19502  vitalilem4  19503  vitalilem5  19504  vitali  19505  mbff  19519  ismbf  19522  ismbfcn  19523  mbfconst  19527  cncombf  19550  cnmbf  19551  0plef  19564  i1fd  19573  itg1ge0  19578  i1faddlem  19585  i1fmullem  19586  i1fadd  19587  i1fmul  19588  itg1addlem4  19591  i1fmulclem  19594  i1fmulc  19595  itg1mulc  19596  i1fsub  19600  itg1sub  19601  itg1lea  19604  itg1le  19605  mbfi1fseqlem2  19608  mbfi1fseqlem4  19610  mbfi1fseqlem5  19611  mbfi1flimlem  19614  mbfmullem2  19616  itg2val  19620  xrge0f  19623  itg2ge0  19627  itg2itg1  19628  itg20  19629  itg2le  19631  itg2const  19632  itg2const2  19633  itg2seq  19634  itg2uba  19635  itg2lea  19636  itg2mulclem  19638  itg2mulc  19639  itg2splitlem  19640  itg2split  19641  itg2monolem1  19642  itg2mono  19645  itg2i1fseqle  19646  itg2i1fseq  19647  itg2addlem  19650  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  iblss  19696  i1fibl  19699  itgitg1  19700  itgle  19701  ibladdlem  19711  itgaddlem1  19714  iblabslem  19719  iblabs  19720  iblabsr  19721  iblmulc2  19722  itgmulc2lem1  19723  bddmulibl  19730  dvf  19794  dvnfre  19838  dvmptcj  19854  dvmptre  19855  dvmptim  19856  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  c1liplem1  19880  c1lip2  19882  dvle  19891  dvivthlem1  19892  dvivth  19894  lhop2  19899  dvcnvrelem2  19902  dvcnvre  19903  dvfsumle  19905  dvfsumge  19906  dvfsumabs  19907  dvfsumlem2  19911  dvfsum2  19918  ftc2  19928  itgparts  19931  itgsubstlem  19932  aalioulem3  20251  taylthlem2  20290  taylth  20291  efcvx  20365  pige3  20425  dvrelog  20528  advlog  20545  advlogexp  20546  logccv  20554  dvcxp1  20626  loglesqr  20642  dmarea  20796  divsqrsumlem  20818  logexprlim  21009  vmadivsum  21176  rpvmasumlem  21181  mudivsum  21224  logdivsum  21227  log2sumbnd  21238  selberglem1  21239  selberglem2  21240  selberg2lem  21244  selberg2  21245  pntrsumo1  21259  selbergr  21262  xrge0tsmsd  24223  replusg  24271  remulr  24272  rele2  24275  raddcn  24315  reust  24344  rrhcn  24380  rrhre  24387  dmvlsiga  24512  mbfmcnt  24618  sxbrsigalem0  24621  sxbrsigalem3  24622  dya2icoseg2  24628  sxbrsigalem2  24636  sitmcl  24663  isrrvv  24701  dstfrvclim1  24735  lgamgulmlem2  24814  erdsze2lem1  24889  erdsze2lem2  24890  snmlval  25018  elee  25833  mblfinlem3  26245  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  itg2gt0cn  26260  ibladdnclem  26261  itgaddnclem1  26263  iblabsnclem  26268  iblabsnc  26269  iblmulc2nc  26270  itgmulc2nclem1  26271  bddiblnc  26275  ftc1anclem3  26282  ftc1anclem4  26283  ftc1anclem5  26284  ftc1anclem6  26285  ftc1anclem7  26286  ftc1anclem8  26287  ftc1anc  26288  ftc2nc  26289  dvreasin  26290  dvreacos  26291  areacirclem1  26292  filbcmb  26442  rrncmslem  26541  repwsmet  26543  rrnequiv  26544  ismrer1  26547  pell1qrval  26909  pell14qrval  26911  pell1234qrval  26913  lhe4.4ex1a  27523  addrval  27647  subrval  27648  mulvval  27649  climreeq  27715  dvcosre  27717  itgsin0pilem1  27720  itgsinexplem1  27724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-cnex 9046  ax-resscn 9047
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator