Theorem reex 9037

Description: The real numbers form a set. See also reexALT 10562. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9027	. 2 |- CC e. _V
2		ax-resscn 9003	. 2 |- RR C_ CC
3	1, 2	ssexi 4308	1 |- RR e. _V

Syntax hints:   e. wcel 1721   _Vcvv 2916   CCcc 8944   RRcr 8945

This theorem is referenced by:  xrex  10565  limsuple  12227  limsuplt  12228  limsupbnd1  12231  rlim  12244  rlimf  12250  rlimss  12251  ello12  12265  lo1f  12267  lo1dm  12268  elo12  12276  o1f  12278  o1dm  12279  o1of2  12361  o1rlimmul  12367  o1add2  12372  o1mul2  12373  o1sub2  12374  o1dif  12378  caucvgrlem  12421  fsumo1  12546  rpnnen  12781  cpnnen  12783  ruclem13  12796  ruc  12797  aleph1re  12799  aleph1irr  12800  cnfldds  16668  ismet  18306  tngngp2  18646  tngngpd  18647  tngngp  18648  tngnrg  18663  rerest  18788  xrtgioo  18790  xrrest  18791  xrsmopn  18796  opnreen  18815  rectbntr0  18816  xrge0tsms  18818  bcthlem1  19230  bcthlem5  19234  pmltpclem2  19299  ovolficcss  19319  ovolval  19323  elovolm  19324  elovolmr  19325  ovolmge0  19326  ovolgelb  19329  ovolctb2  19341  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovolshftlem2  19359  ovolicc2  19371  ismbl  19375  mblsplit  19381  voliunlem2  19398  voliunlem3  19399  ioombl1  19409  dyadmbl  19445  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbff  19472  ismbf  19475  ismbfcn  19476  mbfconst  19480  cncombf  19503  cnmbf  19504  0plef  19517  i1fd  19526  itg1ge0  19531  i1faddlem  19538  i1fmullem  19539  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulclem  19547  i1fmulc  19548  itg1mulc  19549  i1fsub  19553  itg1sub  19554  itg1lea  19557  itg1le  19558  mbfi1fseqlem2  19561  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flimlem  19567  mbfmullem2  19569  itg2val  19573  xrge0f  19576  itg2ge0  19580  itg2itg1  19581  itg20  19582  itg2le  19584  itg2const  19585  itg2const2  19586  itg2seq  19587  itg2uba  19588  itg2lea  19589  itg2mulclem  19591  itg2mulc  19592  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2i1fseq  19600  itg2addlem  19603  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  iblss  19649  i1fibl  19652  itgitg1  19653  itgle  19654  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  bddmulibl  19683  dvf  19747  dvnfre  19791  dvmptcj  19807  dvmptre  19808  dvmptim  19809  rolle  19827  cmvth  19828  mvth  19829  dvlip  19830  dvlipcn  19831  c1liplem1  19833  c1lip2  19835  dvle  19844  dvivthlem1  19845  dvivth  19847  lhop2  19852  dvcnvrelem2  19855  dvcnvre  19856  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsum2  19871  ftc2  19881  itgparts  19884  itgsubstlem  19885  aalioulem3  20204  taylthlem2  20243  taylth  20244  efcvx  20318  pige3  20378  dvrelog  20481  advlog  20498  advlogexp  20499  logccv  20507  dvcxp1  20579  loglesqr  20595  dmarea  20749  divsqrsumlem  20771  logexprlim  20962  vmadivsum  21129  rpvmasumlem  21134  mudivsum  21177  logdivsum  21180  log2sumbnd  21191  selberglem1  21192  selberglem2  21193  selberg2lem  21197  selberg2  21198  pntrsumo1  21212  selbergr  21215  xrge0tsmsd  24176  replusg  24224  remulr  24225  rele2  24228  raddcn  24268  reust  24297  rrhcn  24333  rrhre  24340  dmvlsiga  24465  mbfmcnt  24571  sxbrsigalem0  24574  sxbrsigalem3  24575  dya2icoseg2  24581  sxbrsigalem2  24589  sitmcl  24616  isrrvv  24654  dstfrvclim1  24688  lgamgulmlem2  24767  erdsze2lem1  24842  erdsze2lem2  24843  snmlval  24971  elee  25737  mblfinlem2  26144  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  bddiblnc  26174  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem3  26182  filbcmb  26332  rrncmslem  26431  repwsmet  26433  rrnequiv  26434  ismrer1  26437  pell1qrval  26799  pell14qrval  26801  pell1234qrval  26803  lhe4.4ex1a  27414  addrval  27538  subrval  27539  mulvval  27540  climreeq  27606  dvcosre  27608  itgsin0pilem1  27611  itgsinexplem1  27615

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 2385  ax-sep 4290  ax-cnex 9002  ax-resscn 9003

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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294