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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 9035 . 2  |-  CC  e.  _V
2 ax-resscn 9011 . 2  |-  RR  C_  CC
31, 2ssexi 4316 1  |-  RR  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2924   CCcc 8952   RRcr 8953
This theorem is referenced by:  xrex  10573  limsuple  12235  limsuplt  12236  limsupbnd1  12239  rlim  12252  rlimf  12258  rlimss  12259  ello12  12273  lo1f  12275  lo1dm  12276  elo12  12284  o1f  12286  o1dm  12287  o1of2  12369  o1rlimmul  12375  o1add2  12380  o1mul2  12381  o1sub2  12382  o1dif  12386  caucvgrlem  12429  fsumo1  12554  rpnnen  12789  cpnnen  12791  ruclem13  12804  ruc  12805  aleph1re  12807  aleph1irr  12808  cnfldds  16676  ismet  18314  tngngp2  18654  tngngpd  18655  tngngp  18656  tngnrg  18671  rerest  18796  xrtgioo  18798  xrrest  18799  xrsmopn  18804  opnreen  18823  rectbntr0  18824  xrge0tsms  18826  bcthlem1  19238  bcthlem5  19242  pmltpclem2  19307  ovolficcss  19327  ovolval  19331  elovolm  19332  elovolmr  19333  ovolmge0  19334  ovolgelb  19337  ovolctb2  19349  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovolshftlem2  19367  ovolicc2  19379  ismbl  19383  mblsplit  19389  voliunlem2  19406  voliunlem3  19407  ioombl1  19417  dyadmbl  19453  vitalilem2  19462  vitalilem3  19463  vitalilem4  19464  vitalilem5  19465  vitali  19466  mbff  19480  ismbf  19483  ismbfcn  19484  mbfconst  19488  cncombf  19511  cnmbf  19512  0plef  19525  i1fd  19534  itg1ge0  19539  i1faddlem  19546  i1fmullem  19547  i1fadd  19548  i1fmul  19549  itg1addlem4  19552  i1fmulclem  19555  i1fmulc  19556  itg1mulc  19557  i1fsub  19561  itg1sub  19562  itg1lea  19565  itg1le  19566  mbfi1fseqlem2  19569  mbfi1fseqlem4  19571  mbfi1fseqlem5  19572  mbfi1flimlem  19575  mbfmullem2  19577  itg2val  19581  xrge0f  19584  itg2ge0  19588  itg2itg1  19589  itg20  19590  itg2le  19592  itg2const  19593  itg2const2  19594  itg2seq  19595  itg2uba  19596  itg2lea  19597  itg2mulclem  19599  itg2mulc  19600  itg2splitlem  19601  itg2split  19602  itg2monolem1  19603  itg2mono  19606  itg2i1fseqle  19607  itg2i1fseq  19608  itg2addlem  19611  itg2gt0  19613  itg2cnlem1  19614  itg2cnlem2  19615  iblss  19657  i1fibl  19660  itgitg1  19661  itgle  19662  ibladdlem  19672  itgaddlem1  19675  iblabslem  19680  iblabs  19681  iblabsr  19682  iblmulc2  19683  itgmulc2lem1  19684  bddmulibl  19691  dvf  19755  dvnfre  19799  dvmptcj  19815  dvmptre  19816  dvmptim  19817  rolle  19835  cmvth  19836  mvth  19837  dvlip  19838  dvlipcn  19839  c1liplem1  19841  c1lip2  19843  dvle  19852  dvivthlem1  19853  dvivth  19855  lhop2  19860  dvcnvrelem2  19863  dvcnvre  19864  dvfsumle  19866  dvfsumge  19867  dvfsumabs  19868  dvfsumlem2  19872  dvfsum2  19879  ftc2  19889  itgparts  19892  itgsubstlem  19893  aalioulem3  20212  taylthlem2  20251  taylth  20252  efcvx  20326  pige3  20386  dvrelog  20489  advlog  20506  advlogexp  20507  logccv  20515  dvcxp1  20587  loglesqr  20603  dmarea  20757  divsqrsumlem  20779  logexprlim  20970  vmadivsum  21137  rpvmasumlem  21142  mudivsum  21185  logdivsum  21188  log2sumbnd  21199  selberglem1  21200  selberglem2  21201  selberg2lem  21205  selberg2  21206  pntrsumo1  21220  selbergr  21223  xrge0tsmsd  24184  replusg  24232  remulr  24233  rele2  24236  raddcn  24276  reust  24305  rrhcn  24341  rrhre  24348  dmvlsiga  24473  mbfmcnt  24579  sxbrsigalem0  24582  sxbrsigalem3  24583  dya2icoseg2  24589  sxbrsigalem2  24597  sitmcl  24624  isrrvv  24662  dstfrvclim1  24696  lgamgulmlem2  24775  erdsze2lem1  24850  erdsze2lem2  24851  snmlval  24979  elee  25745  mblfinlem2  26152  itg2addnclem  26163  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  ibladdnclem  26168  itgaddnclem1  26170  iblabsnclem  26175  iblabsnc  26176  iblmulc2nc  26177  itgmulc2nclem1  26178  bddiblnc  26182  dvreasin  26187  dvreacos  26188  areacirclem2  26189  areacirclem3  26190  filbcmb  26340  rrncmslem  26439  repwsmet  26441  rrnequiv  26442  ismrer1  26445  pell1qrval  26807  pell14qrval  26809  pell1234qrval  26811  lhe4.4ex1a  27422  addrval  27546  subrval  27547  mulvval  27548  climreeq  27614  dvcosre  27616  itgsin0pilem1  27619  itgsinexplem1  27623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-cnex 9010  ax-resscn 9011
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator