Theorem reex 9494

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

Assertion

Ref	Expression
reex	|- RR e. _V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9484	. 2 |- CC e. _V
2		ax-resscn 9460	. 2 |- RR C_ CC
3	1, 2	ssexi 4510	1 |- RR e. _V

Syntax hints:   e. wcel 1826   _Vcvv 3034   CCcc 9401   RRcr 9402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-cnex 9459  ax-resscn 9460

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403

This theorem is referenced by:  reelprrecn  9495  xrex  11136  limsuple  13303  limsuplt  13304  limsupbnd1  13307  rlim  13320  rlimf  13326  rlimss  13327  ello12  13341  lo1f  13343  lo1dm  13344  elo12  13352  o1f  13354  o1dm  13355  o1of2  13437  o1rlimmul  13443  o1add2  13448  o1mul2  13449  o1sub2  13450  o1dif  13454  caucvgrlem  13497  fsumo1  13628  rpnnen  13962  cpnnen  13964  ruclem13  13977  ruc  13978  aleph1re  13980  aleph1irr  13981  cnfldds  18543  replusg  18737  remulr  18738  rele2  18741  reds  18743  refldcj  18747  ismet  20911  tngngp2  21251  tngngpd  21252  tngngp  21253  tngnrg  21268  rerest  21394  xrtgioo  21396  xrrest  21397  xrsmopn  21402  opnreen  21421  rectbntr0  21422  xrge0tsms  21424  bcthlem1  21848  bcthlem5  21852  reust  21898  rrxip  21907  pmltpclem2  21946  ovolficcss  21966  ovolval  21970  elovolm  21971  elovolmr  21972  ovolmge0  21973  ovolgelb  21976  ovolctb2  21988  ovolunlem1a  21992  ovolunlem1  21993  ovoliunlem1  21998  ovoliunlem2  21999  ovolshftlem2  22006  ovolicc2  22018  ismbl  22022  mblsplit  22028  voliunlem3  22047  ioombl1  22057  dyadmbl  22094  vitalilem2  22103  vitalilem3  22104  vitalilem4  22105  vitalilem5  22106  vitali  22107  mbff  22119  ismbf  22122  ismbfcn  22123  mbfconst  22127  cncombf  22150  cnmbf  22151  0plef  22164  i1fd  22173  itg1ge0  22178  i1faddlem  22185  i1fmullem  22186  i1fadd  22187  i1fmul  22188  itg1addlem4  22191  i1fmulclem  22194  i1fmulc  22195  itg1mulc  22196  i1fsub  22200  itg1sub  22201  itg1lea  22204  itg1le  22205  mbfi1fseqlem2  22208  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  mbfi1flimlem  22214  mbfmullem2  22216  itg2val  22220  xrge0f  22223  itg2ge0  22227  itg2itg1  22228  itg20  22229  itg2le  22231  itg2const  22232  itg2const2  22233  itg2seq  22234  itg2uba  22235  itg2lea  22236  itg2mulclem  22238  itg2mulc  22239  itg2splitlem  22240  itg2split  22241  itg2monolem1  22242  itg2mono  22245  itg2i1fseqle  22246  itg2i1fseq  22247  itg2addlem  22250  itg2gt0  22252  itg2cnlem1  22253  itg2cnlem2  22254  iblss  22296  i1fibl  22299  itgitg1  22300  itgle  22301  ibladdlem  22311  itgaddlem1  22314  iblabslem  22319  iblabs  22320  iblabsr  22321  iblmulc2  22322  itgmulc2lem1  22323  bddmulibl  22330  dvnfre  22440  c1liplem1  22482  c1lip2  22484  lhop2  22501  dvcnvrelem2  22504  taylthlem2  22854  dmarea  23404  vmadivsum  23784  rpvmasumlem  23789  mudivsum  23832  selberglem1  23847  selberglem2  23848  selberg2lem  23852  selberg2  23853  pntrsumo1  23867  selbergr  23870  iscgrgd  24025  elee  24318  xrge0tsmsd  27929  nn0omnd  27985  xrge0slmod  27988  raddcn  28065  rrhcn  28131  dmvlsiga  28278  ddeval1  28362  ddeval0  28363  ddemeas  28364  mbfmcnt  28395  sxbrsigalem0  28398  sxbrsigalem3  28399  sxbrsigalem2  28413  isrrvv  28565  dstfrvclim1  28599  signsplypnf  28690  erdsze2lem1  28836  erdsze2lem2  28837  snmlval  28965  mblfinlem3  30218  itg2addnclem  30232  itg2addnclem3  30234  itg2addnc  30235  itg2gt0cn  30236  ibladdnclem  30237  itgaddnclem1  30239  iblabsnclem  30244  iblabsnc  30245  iblmulc2nc  30246  itgmulc2nclem1  30247  bddiblnc  30251  ftc1anclem3  30258  ftc1anclem4  30259  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  filbcmb  30397  rrncmslem  30494  repwsmet  30496  rrnequiv  30497  ismrer1  30500  pell1qrval  30947  pell14qrval  30949  pell1234qrval  30951  addrval  31543  subrval  31544  mulvval  31545  climreeq  31785  limsupre  31813  limcresiooub  31814  limcresioolb  31815  icccncfext  31856  cncfiooicclem1  31862  itgsubsticclem  31940  dirkerval  32039  dirkercncflem4  32054  fourierdlem14  32069  fourierdlem15  32070  fourierdlem32  32087  fourierdlem33  32088  fourierdlem54  32109  fourierdlem62  32117  fourierdlem70  32125  fourierdlem81  32136  fourierdlem92  32147  fourierdlem102  32157  fourierdlem111  32166  fourierdlem114  32169  etransclem2  32185  refdivpm  33365  elbigo2  33373  elbigof  33375  elbigodm  33376  elbigoimp  33377  elbigolo1  33378