Theorem reex 9394

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9384	. 2 |- CC e. _V
2		ax-resscn 9360	. 2 |- RR C_ CC
3	1, 2	ssexi 4458	1 |- RR e. _V

Syntax hints:   e. wcel 1756   _Vcvv 2993   CCcc 9301   RRcr 9302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-cnex 9359  ax-resscn 9360

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363

This theorem is referenced by:  reelprrecn  9395  xrex  11009  limsuple  12977  limsuplt  12978  limsupbnd1  12981  rlim  12994  rlimf  13000  rlimss  13001  ello12  13015  lo1f  13017  lo1dm  13018  elo12  13026  o1f  13028  o1dm  13029  o1of2  13111  o1rlimmul  13117  o1add2  13122  o1mul2  13123  o1sub2  13124  o1dif  13128  caucvgrlem  13171  fsumo1  13296  rpnnen  13530  cpnnen  13532  ruclem13  13545  ruc  13546  aleph1re  13548  aleph1irr  13549  cnfldds  17850  replusg  18062  remulr  18063  rele2  18066  reds  18068  refldcj  18072  ismet  19920  tngngp2  20260  tngngpd  20261  tngngp  20262  tngnrg  20277  rerest  20403  xrtgioo  20405  xrrest  20406  xrsmopn  20411  opnreen  20430  rectbntr0  20431  xrge0tsms  20433  bcthlem1  20857  bcthlem5  20861  reust  20907  rrxip  20916  pmltpclem2  20955  ovolficcss  20975  ovolval  20979  elovolm  20980  elovolmr  20981  ovolmge0  20982  ovolgelb  20985  ovolctb2  20997  ovolunlem1a  21001  ovolunlem1  21002  ovoliunlem1  21007  ovoliunlem2  21008  ovolshftlem2  21015  ovolicc2  21027  ismbl  21031  mblsplit  21037  voliunlem3  21055  ioombl1  21065  dyadmbl  21102  vitalilem2  21111  vitalilem3  21112  vitalilem4  21113  vitalilem5  21114  vitali  21115  mbff  21127  ismbf  21130  ismbfcn  21131  mbfconst  21135  cncombf  21158  cnmbf  21159  0plef  21172  i1fd  21181  itg1ge0  21186  i1faddlem  21193  i1fmullem  21194  i1fadd  21195  i1fmul  21196  itg1addlem4  21199  i1fmulclem  21202  i1fmulc  21203  itg1mulc  21204  i1fsub  21208  itg1sub  21209  itg1lea  21212  itg1le  21213  mbfi1fseqlem2  21216  mbfi1fseqlem4  21218  mbfi1fseqlem5  21219  mbfi1flimlem  21222  mbfmullem2  21224  itg2val  21228  xrge0f  21231  itg2ge0  21235  itg2itg1  21236  itg20  21237  itg2le  21239  itg2const  21240  itg2const2  21241  itg2seq  21242  itg2uba  21243  itg2lea  21244  itg2mulclem  21246  itg2mulc  21247  itg2splitlem  21248  itg2split  21249  itg2monolem1  21250  itg2mono  21253  itg2i1fseqle  21254  itg2i1fseq  21255  itg2addlem  21258  itg2gt0  21260  itg2cnlem1  21261  itg2cnlem2  21262  iblss  21304  i1fibl  21307  itgitg1  21308  itgle  21309  ibladdlem  21319  itgaddlem1  21322  iblabslem  21327  iblabs  21328  iblabsr  21329  iblmulc2  21330  itgmulc2lem1  21331  bddmulibl  21338  dvnfre  21448  c1liplem1  21490  c1lip2  21492  lhop2  21509  dvcnvrelem2  21512  taylthlem2  21861  dmarea  22373  vmadivsum  22753  rpvmasumlem  22758  mudivsum  22801  selberglem1  22816  selberglem2  22817  selberg2lem  22821  selberg2  22822  pntrsumo1  22836  selbergr  22839  iscgrgd  22988  elee  23162  xrge0tsmsd  26275  nn0omnd  26331  xrge0slmod  26334  raddcn  26381  rrhcn  26448  dmvlsiga  26594  ddeval1  26672  ddeval0  26673  ddemeas  26674  mbfmcnt  26705  sxbrsigalem0  26708  sxbrsigalem3  26709  sxbrsigalem2  26723  isrrvv  26848  dstfrvclim1  26882  signsplypnf  26973  erdsze2lem1  27113  erdsze2lem2  27114  snmlval  27242  mblfinlem3  28456  itg2addnclem  28469  itg2addnclem3  28471  itg2addnc  28472  itg2gt0cn  28473  ibladdnclem  28474  itgaddnclem1  28476  iblabsnclem  28481  iblabsnc  28482  iblmulc2nc  28483  itgmulc2nclem1  28484  bddiblnc  28488  ftc1anclem3  28495  ftc1anclem4  28496  ftc1anclem5  28497  ftc1anclem6  28498  ftc1anclem7  28499  ftc1anclem8  28500  ftc1anc  28501  filbcmb  28660  rrncmslem  28757  repwsmet  28759  rrnequiv  28760  ismrer1  28763  pell1qrval  29213  pell14qrval  29215  pell1234qrval  29217  addrval  29748  subrval  29749  mulvval  29750  climreeq  29812