Theorem reex 9583

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9573	. 2 |- CC e. _V
2		ax-resscn 9549	. 2 |- RR C_ CC
3	1, 2	ssexi 4592	1 |- RR e. _V

Syntax hints:   e. wcel 1767   _Vcvv 3113   CCcc 9490   RRcr 9491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-cnex 9548  ax-resscn 9549

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490

This theorem is referenced by:  reelprrecn  9584  xrex  11217  limsuple  13264  limsuplt  13265  limsupbnd1  13268  rlim  13281  rlimf  13287  rlimss  13288  ello12  13302  lo1f  13304  lo1dm  13305  elo12  13313  o1f  13315  o1dm  13316  o1of2  13398  o1rlimmul  13404  o1add2  13409  o1mul2  13410  o1sub2  13411  o1dif  13415  caucvgrlem  13458  fsumo1  13589  rpnnen  13821  cpnnen  13823  ruclem13  13836  ruc  13837  aleph1re  13839  aleph1irr  13840  cnfldds  18229  replusg  18441  remulr  18442  rele2  18445  reds  18447  refldcj  18451  ismet  20589  tngngp2  20929  tngngpd  20930  tngngp  20931  tngnrg  20946  rerest  21072  xrtgioo  21074  xrrest  21075  xrsmopn  21080  opnreen  21099  rectbntr0  21100  xrge0tsms  21102  bcthlem1  21526  bcthlem5  21530  reust  21576  rrxip  21585  pmltpclem2  21624  ovolficcss  21644  ovolval  21648  elovolm  21649  elovolmr  21650  ovolmge0  21651  ovolgelb  21654  ovolctb2  21666  ovolunlem1a  21670  ovolunlem1  21671  ovoliunlem1  21676  ovoliunlem2  21677  ovolshftlem2  21684  ovolicc2  21696  ismbl  21700  mblsplit  21706  voliunlem3  21725  ioombl1  21735  dyadmbl  21772  vitalilem2  21781  vitalilem3  21782  vitalilem4  21783  vitalilem5  21784  vitali  21785  mbff  21797  ismbf  21800  ismbfcn  21801  mbfconst  21805  cncombf  21828  cnmbf  21829  0plef  21842  i1fd  21851  itg1ge0  21856  i1faddlem  21863  i1fmullem  21864  i1fadd  21865  i1fmul  21866  itg1addlem4  21869  i1fmulclem  21872  i1fmulc  21873  itg1mulc  21874  i1fsub  21878  itg1sub  21879  itg1lea  21882  itg1le  21883  mbfi1fseqlem2  21886  mbfi1fseqlem4  21888  mbfi1fseqlem5  21889  mbfi1flimlem  21892  mbfmullem2  21894  itg2val  21898  xrge0f  21901  itg2ge0  21905  itg2itg1  21906  itg20  21907  itg2le  21909  itg2const  21910  itg2const2  21911  itg2seq  21912  itg2uba  21913  itg2lea  21914  itg2mulclem  21916  itg2mulc  21917  itg2splitlem  21918  itg2split  21919  itg2monolem1  21920  itg2mono  21923  itg2i1fseqle  21924  itg2i1fseq  21925  itg2addlem  21928  itg2gt0  21930  itg2cnlem1  21931  itg2cnlem2  21932  iblss  21974  i1fibl  21977  itgitg1  21978  itgle  21979  ibladdlem  21989  itgaddlem1  21992  iblabslem  21997  iblabs  21998  iblabsr  21999  iblmulc2  22000  itgmulc2lem1  22001  bddmulibl  22008  dvnfre  22118  c1liplem1  22160  c1lip2  22162  lhop2  22179  dvcnvrelem2  22182  taylthlem2  22531  dmarea  23043  vmadivsum  23423  rpvmasumlem  23428  mudivsum  23471  selberglem1  23486  selberglem2  23487  selberg2lem  23491  selberg2  23492  pntrsumo1  23506  selbergr  23509  iscgrgd  23661  elee  23901  xrge0tsmsd  27466  nn0omnd  27522  xrge0slmod  27525  raddcn  27575  rrhcn  27642  dmvlsiga  27797  ddeval1  27874  ddeval0  27875  ddemeas  27876  mbfmcnt  27907  sxbrsigalem0  27910  sxbrsigalem3  27911  sxbrsigalem2  27925  isrrvv  28050  dstfrvclim1  28084  signsplypnf  28175  erdsze2lem1  28315  erdsze2lem2  28316  snmlval  28444  mblfinlem3  29658  itg2addnclem  29671  itg2addnclem3  29673  itg2addnc  29674  itg2gt0cn  29675  ibladdnclem  29676  itgaddnclem1  29678  iblabsnclem  29683  iblabsnc  29684  iblmulc2nc  29685  itgmulc2nclem1  29686  bddiblnc  29690  ftc1anclem3  29697  ftc1anclem4  29698  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  filbcmb  29862  rrncmslem  29959  repwsmet  29961  rrnequiv  29962  ismrer1  29965  pell1qrval  30414  pell14qrval  30416  pell1234qrval  30418  addrval  30981  subrval  30982  mulvval  30983  tgiooss  31138  climreeq  31183  limsupre  31211  limcresiooub  31212  limcresioolb  31213  icccncfext  31254  cncfiooicclem1  31260  dvcnre  31272  itgsubsticclem  31321  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  dirkerval  31419  dirkeritg  31430  dirkercncflem2  31432  dirkercncflem4  31434  fourierdlem14  31449  fourierdlem15  31450  fourierdlem28  31463  fourierdlem32  31467  fourierdlem33  31468  fourierdlem39  31474  fourierdlem54  31489  fourierdlem56  31491  fourierdlem57  31492  fourierdlem58  31493  fourierdlem59  31494  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem68  31503  fourierdlem70  31505  fourierdlem72  31507  fourierdlem81  31516  fourierdlem92  31527  fourierdlem102  31537  fourierdlem111  31546  fourierdlem114  31549