Theorem reex 9361

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9351	. 2 |- CC e. _V
2		ax-resscn 9327	. 2 |- RR C_ CC
3	1, 2	ssexi 4425	1 |- RR e. _V

Syntax hints:   e. wcel 1755   _Vcvv 2962   CCcc 9268   RRcr 9269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-cnex 9326  ax-resscn 9327

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330

This theorem is referenced by:  reelprrecn  9362  xrex  10976  limsuple  12940  limsuplt  12941  limsupbnd1  12944  rlim  12957  rlimf  12963  rlimss  12964  ello12  12978  lo1f  12980  lo1dm  12981  elo12  12989  o1f  12991  o1dm  12992  o1of2  13074  o1rlimmul  13080  o1add2  13085  o1mul2  13086  o1sub2  13087  o1dif  13091  caucvgrlem  13134  fsumo1  13258  rpnnen  13492  cpnnen  13494  ruclem13  13507  ruc  13508  aleph1re  13510  aleph1irr  13511  cnfldds  17672  replusg  17882  remulr  17883  rele2  17886  reds  17888  refldcj  17892  ismet  19740  tngngp2  20080  tngngpd  20081  tngngp  20082  tngnrg  20097  rerest  20223  xrtgioo  20225  xrrest  20226  xrsmopn  20231  opnreen  20250  rectbntr0  20251  xrge0tsms  20253  bcthlem1  20677  bcthlem5  20681  reust  20727  rrxip  20736  pmltpclem2  20775  ovolficcss  20795  ovolval  20799  elovolm  20800  elovolmr  20801  ovolmge0  20802  ovolgelb  20805  ovolctb2  20817  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovolshftlem2  20835  ovolicc2  20847  ismbl  20851  mblsplit  20857  voliunlem3  20875  ioombl1  20885  dyadmbl  20922  vitalilem2  20931  vitalilem3  20932  vitalilem4  20933  vitalilem5  20934  vitali  20935  mbff  20947  ismbf  20950  ismbfcn  20951  mbfconst  20955  cncombf  20978  cnmbf  20979  0plef  20992  i1fd  21001  itg1ge0  21006  i1faddlem  21013  i1fmullem  21014  i1fadd  21015  i1fmul  21016  itg1addlem4  21019  i1fmulclem  21022  i1fmulc  21023  itg1mulc  21024  i1fsub  21028  itg1sub  21029  itg1lea  21032  itg1le  21033  mbfi1fseqlem2  21036  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1flimlem  21042  mbfmullem2  21044  itg2val  21048  xrge0f  21051  itg2ge0  21055  itg2itg1  21056  itg20  21057  itg2le  21059  itg2const  21060  itg2const2  21061  itg2seq  21062  itg2uba  21063  itg2lea  21064  itg2mulclem  21066  itg2mulc  21067  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  itg2mono  21073  itg2i1fseqle  21074  itg2i1fseq  21075  itg2addlem  21078  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  iblss  21124  i1fibl  21127  itgitg1  21128  itgle  21129  ibladdlem  21139  itgaddlem1  21142  iblabslem  21147  iblabs  21148  iblabsr  21149  iblmulc2  21150  itgmulc2lem1  21151  bddmulibl  21158  dvnfre  21268  c1liplem1  21310  c1lip2  21312  lhop2  21329  dvcnvrelem2  21332  taylthlem2  21724  dmarea  22236  vmadivsum  22616  rpvmasumlem  22621  mudivsum  22664  selberglem1  22679  selberglem2  22680  selberg2lem  22684  selberg2  22685  pntrsumo1  22699  selbergr  22702  iscgrgd  22847  elee  22963  xrge0tsmsd  26106  nn0omnd  26163  xrge0slmod  26166  raddcn  26213  rrhcn  26280  dmvlsiga  26426  ddeval1  26504  ddeval0  26505  ddemeas  26506  mbfmcnt  26537  sxbrsigalem0  26540  sxbrsigalem3  26541  sxbrsigalem2  26555  isrrvv  26674  dstfrvclim1  26708  signsplypnf  26799  erdsze2lem1  26939  erdsze2lem2  26940  snmlval  27068  mblfinlem3  28274  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  itg2gt0cn  28291  ibladdnclem  28292  itgaddnclem1  28294  iblabsnclem  28299  iblabsnc  28300  iblmulc2nc  28301  itgmulc2nclem1  28302  bddiblnc  28306  ftc1anclem3  28313  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  filbcmb  28478  rrncmslem  28575  repwsmet  28577  rrnequiv  28578  ismrer1  28581  pell1qrval  29032  pell14qrval  29034  pell1234qrval  29036  addrval  29567  subrval  29568  mulvval  29569  climreeq  29632