Theorem reex 9648

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9638	. 2 |- CC e. _V
2		ax-resscn 9614	. 2 |- RR C_ CC
3	1, 2	ssexi 4541	1 |- RR e. _V

Syntax hints:   e. wcel 1904   _Vcvv 3031   CCcc 9555   RRcr 9556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-cnex 9613  ax-resscn 9614

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404

This theorem is referenced by:  reelprrecn  9649  negfi  10576  xrex  11322  limsuple  13613  limsupleOLD  13614  limsuplt  13615  limsupltOLD  13616  limsupbnd1  13621  limsupbnd1OLD  13622  rlim  13636  rlimf  13642  rlimss  13643  ello12  13657  lo1f  13659  lo1dm  13660  elo12  13668  o1f  13670  o1dm  13671  o1of2  13753  o1rlimmul  13759  o1add2  13764  o1mul2  13765  o1sub2  13766  o1dif  13770  caucvgrlem  13813  caucvgrlemOLD  13814  fsumo1  13949  rpnnen  14356  cpnnen  14358  ruclem13  14371  ruc  14372  aleph1re  14374  aleph1irr  14375  cnfldds  19057  replusg  19255  remulr  19256  rele2  19259  reds  19261  refldcj  19265  ismet  21416  tngngp2  21738  tngngpd  21739  tngngp  21740  tngnrg  21755  rerest  21900  xrtgioo  21902  xrrest  21903  xrsmopn  21908  opnreen  21927  rectbntr0  21928  xrge0tsms  21930  bcthlem1  22370  bcthlem5  22374  reust  22418  rrxip  22427  pmltpclem2  22478  ovolficcss  22500  ovolval  22504  ovolvalOLD  22505  elovolm  22506  elovolmr  22507  ovolmge0  22508  ovolgelb  22511  ovolctb2  22523  ovolunlem1a  22527  ovolunlem1  22528  ovoliunlem1  22533  ovoliunlem2  22534  ovolshftlem2  22541  ovolicc2  22554  ismbl  22558  mblsplit  22564  voliunlem3  22584  ioombl1  22594  dyadmbl  22637  vitalilem2  22646  vitalilem3  22647  vitalilem4  22648  vitalilem5  22649  vitali  22650  mbff  22662  ismbf  22665  ismbfcn  22666  mbfconst  22670  cncombf  22693  cnmbf  22694  0plef  22709  i1fd  22718  itg1ge0  22723  i1faddlem  22730  i1fmullem  22731  i1fadd  22732  i1fmul  22733  itg1addlem4  22736  i1fmulclem  22739  i1fmulc  22740  itg1mulc  22741  i1fsub  22745  itg1sub  22746  itg1lea  22749  itg1le  22750  mbfi1fseqlem2  22753  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfi1flimlem  22759  mbfmullem2  22761  itg2val  22765  xrge0f  22768  itg2ge0  22772  itg2itg1  22773  itg20  22774  itg2le  22776  itg2const  22777  itg2const2  22778  itg2seq  22779  itg2uba  22780  itg2lea  22781  itg2mulclem  22783  itg2mulc  22784  itg2splitlem  22785  itg2split  22786  itg2monolem1  22787  itg2mono  22790  itg2i1fseqle  22791  itg2i1fseq  22792  itg2addlem  22795  itg2gt0  22797  itg2cnlem1  22798  itg2cnlem2  22799  iblss  22841  i1fibl  22844  itgitg1  22845  itgle  22846  ibladdlem  22856  itgaddlem1  22859  iblabslem  22864  iblabs  22865  iblabsr  22866  iblmulc2  22867  itgmulc2lem1  22868  bddmulibl  22875  dvnfre  22985  c1liplem1  23027  c1lip2  23029  lhop2  23046  dvcnvrelem2  23049  taylthlem2  23408  dmarea  23962  vmadivsum  24399  rpvmasumlem  24404  mudivsum  24447  selberglem1  24462  selberglem2  24463  selberg2lem  24467  selberg2  24468  pntrsumo1  24482  selbergr  24485  iscgrgd  24637  elee  25003  xrge0tsmsd  28622  nn0omnd  28678  xrge0slmod  28681  raddcn  28809  rrhcn  28875  qqtopn  28889  dmvlsiga  29025  ddeval1  29130  ddeval0  29131  ddemeas  29132  mbfmcnt  29163  sxbrsigalem0  29166  sxbrsigalem3  29167  sxbrsigalem2  29181  isrrvv  29349  dstfrvclim1  29383  signsplypnf  29511  erdsze2lem1  29998  erdsze2lem2  29999  snmlval  30126  icoreresf  31825  icoreval  31826  poimirlem29  32033  poimirlem30  32034  poimirlem31  32035  poimir  32037  broucube  32038  mblfinlem3  32043  itg2addnclem  32057  itg2addnclem3  32059  itg2addnc  32060  itg2gt0cn  32061  ibladdnclem  32062  itgaddnclem1  32064  iblabsnclem  32069  iblabsnc  32070  iblmulc2nc  32071  itgmulc2nclem1  32072  bddiblnc  32076  ftc1anclem3  32083  ftc1anclem4  32084  ftc1anclem5  32085  ftc1anclem6  32086  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  filbcmb  32131  rrncmslem  32228  repwsmet  32230  rrnequiv  32231  ismrer1  32234  pell1qrval  35763  pell14qrval  35765  pell1234qrval  35767  addrval  36889  subrval  36890  mulvval  36891  climreeq  37790  limsupre  37818  limsupreOLD  37819  limcresiooub  37820  limcresioolb  37821  icccncfext  37862  cncfiooicclem1  37868  itgsubsticclem  37949  ovolsplit  37963  dirkerval  38065  dirkercncflem4  38080  fourierdlem14  38095  fourierdlem15  38096  fourierdlem32  38114  fourierdlem33  38115  fourierdlem54  38136  fourierdlem62  38144  fourierdlem70  38152  fourierdlem81  38163  fourierdlem92  38174  fourierdlem102  38184  fourierdlem111  38193  fourierdlem114  38196  etransclem2  38213  rrxtopn0  38274  qndenserrnbllem  38275  qndenserrnbl  38276  qndenserrn  38280  dmvolsal  38317  hoicvr  38488  hoissrrn  38489  hoiprodcl2  38495  hoicvrrex  38496  ovn0lem  38505  ovn02  38508  hsphoif  38516  hoidmvval  38517  hoissrrn2  38518  hsphoival  38519  hoidmvlelem3  38537  hoidmvle  38540  ovnhoilem1  38541  ovnhoilem2  38542  ovnhoi  38543  hspval  38549  ovnlecvr2  38550  ovncvr2  38551  hoidifhspval2  38555  hoiqssbl  38565  hspmbllem2  38567  hspmbl  38569  hoimbl  38571  opnvonmbllem2  38573  ovolval2lem  38583  ovolval2  38584  ovolval3  38587  ovolval4lem2  38590  ovolval5lem2  38593  ovnovollem1  38596  ovnovollem2  38597  ovnovollem3  38598  vonvolmbllem  38600  vonvolmbl  38601  refdivpm  40863  elbigo2  40871  elbigof  40873  elbigodm  40874  elbigoimp  40875  elbigolo1  40876