Theorem reex 11120

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11110	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11086	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5259	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11027  ℝcr 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  reelprrecn  11121  negfi  12096  xrex  12928  limsuple  15431  limsuplt  15432  limsupbnd1  15435  rlim  15448  rlimf  15454  rlimss  15455  ello12  15469  lo1f  15471  lo1dm  15472  elo12  15480  o1f  15482  o1dm  15483  o1of2  15566  o1rlimmul  15572  o1add2  15577  o1mul2  15578  o1sub2  15579  o1dif  15583  caucvgrlem  15626  fsumo1  15766  rpnnen  16185  cpnnen  16187  ruclem13  16200  ruc  16201  aleph1re  16203  aleph1irr  16204  cnfldds  21356  cnflddsOLD  21369  replusg  21600  remulr  21601  rele2  21604  reds  21606  refldcj  21610  ismet  24298  tngngp2  24627  tngngpd  24628  tngngp  24629  tngngp3  24631  nrmtngnrm  24633  tngnrg  24649  rerest  24779  xrtgioo  24782  xrrest  24783  xrsmopn  24788  opnreen  24807  rectbntr0  24808  xrge0tsms  24810  bcthlem1  25301  bcthlem5  25305  reust  25358  rrxip  25367  rrx0el  25375  ehl0base  25393  ehl1eudis  25397  ehl2eudis  25399  pmltpclem2  25426  ovolficcss  25446  ovolval  25450  elovolmlem  25451  ovolctb2  25469  ismbl  25503  mblsplit  25509  voliunlem3  25529  dyadmbl  25577  vitalilem2  25586  vitalilem3  25587  vitalilem4  25588  vitalilem5  25589  vitali  25590  mbff  25602  ismbf  25605  ismbfcn  25606  mbfconst  25610  cncombf  25635  cnmbf  25636  0plef  25649  i1fd  25658  itg1ge0  25663  i1faddlem  25670  i1fmullem  25671  i1fadd  25672  i1fmul  25673  itg1addlem4  25676  i1fmulclem  25679  i1fmulc  25680  itg1mulc  25681  i1fsub  25685  itg1sub  25686  itg1lea  25689  itg1le  25690  mbfi1fseqlem2  25693  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1flimlem  25699  mbfmullem2  25701  itg2val  25705  xrge0f  25708  itg2ge0  25712  itg2itg1  25713  itg20  25714  itg2le  25716  itg2const  25717  itg2const2  25718  itg2seq  25719  itg2uba  25720  itg2lea  25721  itg2mulclem  25723  itg2mulc  25724  itg2splitlem  25725  itg2split  25726  itg2monolem1  25727  itg2mono  25730  itg2i1fseqle  25731  itg2i1fseq  25732  itg2addlem  25735  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  iblss  25782  i1fibl  25785  itgitg1  25786  itgle  25787  ibladdlem  25797  itgaddlem1  25800  iblabslem  25805  iblabs  25806  iblabsr  25807  iblmulc2  25808  itgmulc2lem1  25809  bddmulibl  25816  bddiblnc  25819  dvnfre  25929  c1liplem1  25973  c1lip2  25975  lhop2  25992  dvcnvrelem2  25995  taylthlem2  26351  taylthlem2OLD  26352  dmarea  26934  vmadivsum  27459  rpvmasumlem  27464  mudivsum  27507  selberglem1  27522  selberglem2  27523  selberg2lem  27527  selberg2  27528  pntrsumo1  27542  selbergr  27545  iscgrgd  28595  elee  28976  xrge0tsmsd  33149  nn0omnd  33419  xrge0slmod  33423  raddcn  34089  rrhcn  34157  qqtopn  34171  dmvlsiga  34289  ddeval1  34394  ddeval0  34395  ddemeas  34396  mbfmcnt  34428  sxbrsigalem0  34431  sxbrsigalem3  34432  sxbrsigalem2  34446  isrrvv  34603  dstfrvclim1  34638  signsplypnf  34710  erdsze2lem1  35401  erdsze2lem2  35402  snmlval  35529  knoppcnlem5  36773  knoppcnlem6  36774  knoppcnlem7  36775  knoppcnlem8  36776  cnndvlem2  36814  icoreresf  37682  icoreval  37683  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  poimir  37988  broucube  37989  mblfinlem3  37994  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  ibladdnclem  38011  itgaddnclem1  38013  iblabsnclem  38018  iblabsnc  38019  iblmulc2nc  38020  itgmulc2nclem1  38021  ftc1anclem3  38030  ftc1anclem4  38031  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  filbcmb  38075  rrncmslem  38167  repwsmet  38169  rrnequiv  38170  ismrer1  38173  absex  42701  pell1qrval  43292  pell14qrval  43294  pell1234qrval  43296  k0004ss1  44596  addrval  44910  subrval  44911  mulvval  44912  rpex  45794  climreeq  46061  limsupre  46087  limcresiooub  46088  limcresioolb  46089  limsuppnfdlem  46147  limsuppnflem  46156  limsupmnflem  46166  limsupre2lem  46170  xlimclim  46270  icccncfext  46333  cncfiooicclem1  46339  itgsubsticclem  46421  ovolsplit  46434  dirkerval  46537  dirkercncflem4  46552  fourierdlem14  46567  fourierdlem15  46568  fourierdlem32  46585  fourierdlem33  46586  fourierdlem54  46606  fourierdlem62  46614  fourierdlem70  46622  fourierdlem81  46633  fourierdlem92  46644  fourierdlem102  46654  fourierdlem111  46663  fourierdlem114  46666  etransclem2  46682  rrxtopn0  46739  qndenserrnbllem  46740  qndenserrnbl  46741  qndenserrn  46745  rrnprjdstle  46747  ioorrnopnlem  46750  dmvolsal  46792  hoicvr  46994  hoissrrn  46995  hoiprodcl2  47001  hoicvrrex  47002  ovn0lem  47011  ovn02  47014  hsphoif  47022  hoidmvval  47023  hoissrrn2  47024  hsphoival  47025  hoidmvlelem3  47043  hoidmvle  47046  ovnhoilem1  47047  ovnhoilem2  47048  ovnhoi  47049  hspval  47055  ovnlecvr2  47056  ovncvr2  47057  hoidifhspval2  47061  hoiqssbl  47071  hspmbllem2  47073  hspmbl  47075  hoimbl  47077  opnvonmbllem2  47079  ovolval2lem  47089  ovolval2  47090  ovolval3  47093  ovolval4lem2  47096  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  ovnovollem3  47104  vonvolmbllem  47106  vonvolmbl  47107  vitali2  47140  issmflem  47173  incsmf  47188  decsmf  47213  nsssmfmbflem  47224  smfresal  47234  smfmullem4  47240  smf2id  47247  nthrucw  47332  refdivpm  49032  elbigo2  49040  elbigof  49042  elbigodm  49043  elbigoimp  49044  elbigolo1  49045  prelrrx2  49201  rrx2xpref1o  49206  rrx2xpreen  49207  rrx2linesl  49231  line2  49240  line2x  49242  line2y  49243  amgmlemALT  50290