Theorem reex 9635

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9625	. 2 |- CC e. _V
2		ax-resscn 9601	. 2 |- RR C_ CC
3	1, 2	ssexi 4551	1 |- RR e. _V

Syntax hints:   e. wcel 1889   _Vcvv 3047   CCcc 9542   RRcr 9543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-cnex 9600  ax-resscn 9601

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-in 3413  df-ss 3420

This theorem is referenced by:  reelprrecn  9636  negfi  10561  xrex  11306  limsuple  13548  limsupleOLD  13549  limsuplt  13550  limsupltOLD  13551  limsupbnd1  13556  limsupbnd1OLD  13557  rlim  13571  rlimf  13577  rlimss  13578  ello12  13592  lo1f  13594  lo1dm  13595  elo12  13603  o1f  13605  o1dm  13606  o1of2  13688  o1rlimmul  13694  o1add2  13699  o1mul2  13700  o1sub2  13701  o1dif  13705  caucvgrlem  13748  caucvgrlemOLD  13749  fsumo1  13884  rpnnen  14291  cpnnen  14293  ruclem13  14306  ruc  14307  aleph1re  14309  aleph1irr  14310  cnfldds  18992  replusg  19190  remulr  19191  rele2  19194  reds  19196  refldcj  19200  ismet  21350  tngngp2  21672  tngngpd  21673  tngngp  21674  tngnrg  21689  rerest  21834  xrtgioo  21836  xrrest  21837  xrsmopn  21842  opnreen  21861  rectbntr0  21862  xrge0tsms  21864  bcthlem1  22304  bcthlem5  22308  reust  22352  rrxip  22361  pmltpclem2  22412  ovolficcss  22434  ovolval  22438  ovolvalOLD  22439  elovolm  22440  elovolmr  22441  ovolmge0  22442  ovolgelb  22445  ovolctb2  22457  ovolunlem1a  22461  ovolunlem1  22462  ovoliunlem1  22467  ovoliunlem2  22468  ovolshftlem2  22475  ovolicc2  22488  ismbl  22492  mblsplit  22498  voliunlem3  22517  ioombl1  22527  dyadmbl  22570  vitalilem2  22579  vitalilem3  22580  vitalilem4  22581  vitalilem5  22582  vitali  22583  mbff  22595  ismbf  22598  ismbfcn  22599  mbfconst  22603  cncombf  22626  cnmbf  22627  0plef  22642  i1fd  22651  itg1ge0  22656  i1faddlem  22663  i1fmullem  22664  i1fadd  22665  i1fmul  22666  itg1addlem4  22669  i1fmulclem  22672  i1fmulc  22673  itg1mulc  22674  i1fsub  22678  itg1sub  22679  itg1lea  22682  itg1le  22683  mbfi1fseqlem2  22686  mbfi1fseqlem4  22688  mbfi1fseqlem5  22689  mbfi1flimlem  22692  mbfmullem2  22694  itg2val  22698  xrge0f  22701  itg2ge0  22705  itg2itg1  22706  itg20  22707  itg2le  22709  itg2const  22710  itg2const2  22711  itg2seq  22712  itg2uba  22713  itg2lea  22714  itg2mulclem  22716  itg2mulc  22717  itg2splitlem  22718  itg2split  22719  itg2monolem1  22720  itg2mono  22723  itg2i1fseqle  22724  itg2i1fseq  22725  itg2addlem  22728  itg2gt0  22730  itg2cnlem1  22731  itg2cnlem2  22732  iblss  22774  i1fibl  22777  itgitg1  22778  itgle  22779  ibladdlem  22789  itgaddlem1  22792  iblabslem  22797  iblabs  22798  iblabsr  22799  iblmulc2  22800  itgmulc2lem1  22801  bddmulibl  22808  dvnfre  22918  c1liplem1  22960  c1lip2  22962  lhop2  22979  dvcnvrelem2  22982  taylthlem2  23341  dmarea  23895  vmadivsum  24332  rpvmasumlem  24337  mudivsum  24380  selberglem1  24395  selberglem2  24396  selberg2lem  24400  selberg2  24401  pntrsumo1  24415  selbergr  24418  iscgrgd  24570  elee  24936  xrge0tsmsd  28560  nn0omnd  28616  xrge0slmod  28619  raddcn  28747  rrhcn  28813  qqtopn  28827  dmvlsiga  28963  ddeval1  29069  ddeval0  29070  ddemeas  29071  mbfmcnt  29102  sxbrsigalem0  29105  sxbrsigalem3  29106  sxbrsigalem2  29120  isrrvv  29288  dstfrvclim1  29322  signsplypnf  29451  erdsze2lem1  29938  erdsze2lem2  29939  snmlval  30066  icoreresf  31767  icoreval  31768  poimirlem29  31981  poimirlem30  31982  poimirlem31  31983  poimir  31985  broucube  31986  mblfinlem3  31991  itg2addnclem  32005  itg2addnclem3  32007  itg2addnc  32008  itg2gt0cn  32009  ibladdnclem  32010  itgaddnclem1  32012  iblabsnclem  32017  iblabsnc  32018  iblmulc2nc  32019  itgmulc2nclem1  32020  bddiblnc  32024  ftc1anclem3  32031  ftc1anclem4  32032  ftc1anclem5  32033  ftc1anclem6  32034  ftc1anclem7  32035  ftc1anclem8  32036  ftc1anc  32037  filbcmb  32079  rrncmslem  32176  repwsmet  32178  rrnequiv  32179  ismrer1  32182  pell1qrval  35704  pell14qrval  35706  pell1234qrval  35708  addrval  36830  subrval  36831  mulvval  36832  climreeq  37703  limsupre  37731  limsupreOLD  37732  limcresiooub  37733  limcresioolb  37734  icccncfext  37775  cncfiooicclem1  37781  itgsubsticclem  37862  dirkerval  37963  dirkercncflem4  37978  fourierdlem14  37993  fourierdlem15  37994  fourierdlem32  38012  fourierdlem33  38013  fourierdlem54  38034  fourierdlem62  38042  fourierdlem70  38050  fourierdlem81  38061  fourierdlem92  38072  fourierdlem102  38082  fourierdlem111  38091  fourierdlem114  38094  etransclem2  38111  rrxtopn0  38172  qndenserrnbllem  38173  qndenserrnbl  38174  qndenserrn  38178  hoicvr  38380  hoissrrn  38381  hoiprodcl2  38387  hoicvrrex  38388  ovn0lem  38397  ovn02  38400  hsphoif  38408  hoidmvval  38409  hoissrrn2  38410  hsphoival  38411  hoidmvlelem3  38429  hoidmvle  38432  ovnhoilem1  38433  ovnhoilem2  38434  ovnhoi  38435  hspval  38441  ovnlecvr2  38442  ovncvr2  38443  hoidifhspval2  38447  hoiqssbl  38457  hspmbllem2  38459  hspmbl  38461  hoimbl  38463  opnvonmbllem2  38465  refdivpm  40459  elbigo2  40467  elbigof  40469  elbigodm  40470  elbigoimp  40471  elbigolo1  40472