Theorem reex 11201

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11191	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11167	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5323	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ℂcc 11108  ℝcr 11109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-cnex 11166  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  reelprrecn  11202  negfi  12163  xrex  12971  limsuple  15422  limsuplt  15423  limsupbnd1  15426  rlim  15439  rlimf  15445  rlimss  15446  ello12  15460  lo1f  15462  lo1dm  15463  elo12  15471  o1f  15473  o1dm  15474  o1of2  15557  o1rlimmul  15563  o1add2  15568  o1mul2  15569  o1sub2  15570  o1dif  15574  caucvgrlem  15619  fsumo1  15758  rpnnen  16170  cpnnen  16172  ruclem13  16185  ruc  16186  aleph1re  16188  aleph1irr  16189  cnfldds  20954  replusg  21163  remulr  21164  rele2  21167  reds  21169  refldcj  21173  ismet  23829  tngngp2  24169  tngngpd  24170  tngngp  24171  tngngp3  24173  nrmtngnrm  24175  tngnrg  24191  rerest  24320  xrtgioo  24322  xrrest  24323  xrsmopn  24328  opnreen  24347  rectbntr0  24348  xrge0tsms  24350  bcthlem1  24841  bcthlem5  24845  reust  24898  rrxip  24907  rrx0el  24915  ehl0base  24933  ehl1eudis  24937  ehl2eudis  24939  pmltpclem2  24966  ovolficcss  24986  ovolval  24990  elovolmlem  24991  ovolctb2  25009  ismbl  25043  mblsplit  25049  voliunlem3  25069  dyadmbl  25117  vitalilem2  25126  vitalilem3  25127  vitalilem4  25128  vitalilem5  25129  vitali  25130  mbff  25142  ismbf  25145  ismbfcn  25146  mbfconst  25150  cncombf  25175  cnmbf  25176  0plef  25189  i1fd  25198  itg1ge0  25203  i1faddlem  25210  i1fmullem  25211  i1fadd  25212  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulclem  25220  i1fmulc  25221  itg1mulc  25222  i1fsub  25226  itg1sub  25227  itg1lea  25230  itg1le  25231  mbfi1fseqlem2  25234  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1flimlem  25240  mbfmullem2  25242  itg2val  25246  xrge0f  25249  itg2ge0  25253  itg2itg1  25254  itg20  25255  itg2le  25257  itg2const  25258  itg2const2  25259  itg2seq  25260  itg2uba  25261  itg2lea  25262  itg2mulclem  25264  itg2mulc  25265  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2addlem  25276  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  iblss  25322  i1fibl  25325  itgitg1  25326  itgle  25327  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgmulc2lem1  25349  bddmulibl  25356  bddiblnc  25359  dvnfre  25469  c1liplem1  25513  c1lip2  25515  lhop2  25532  dvcnvrelem2  25535  taylthlem2  25886  dmarea  26462  vmadivsum  26985  rpvmasumlem  26990  mudivsum  27033  selberglem1  27048  selberglem2  27049  selberg2lem  27053  selberg2  27054  pntrsumo1  27068  selbergr  27071  iscgrgd  27764  elee  28152  xrge0tsmsd  32209  nn0omnd  32460  xrge0slmod  32463  raddcn  32909  rrhcn  32977  qqtopn  32991  dmvlsiga  33127  ddeval1  33232  ddeval0  33233  ddemeas  33234  mbfmcnt  33267  sxbrsigalem0  33270  sxbrsigalem3  33271  sxbrsigalem2  33285  isrrvv  33442  dstfrvclim1  33476  signsplypnf  33561  erdsze2lem1  34194  erdsze2lem2  34195  snmlval  34322  knoppcnlem5  35373  knoppcnlem6  35374  knoppcnlem7  35375  knoppcnlem8  35376  cnndvlem2  35414  icoreresf  36233  icoreval  36234  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimir  36521  broucube  36522  mblfinlem3  36527  itg2addnclem  36539  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nclem1  36554  ftc1anclem3  36563  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  filbcmb  36608  rrncmslem  36700  repwsmet  36702  rrnequiv  36703  ismrer1  36706  pell1qrval  41584  pell14qrval  41586  pell1234qrval  41588  k0004ss1  42902  addrval  43225  subrval  43226  mulvval  43227  climreeq  44329  limsupre  44357  limcresiooub  44358  limcresioolb  44359  limsuppnfdlem  44417  limsuppnflem  44426  limsupmnflem  44436  limsupre2lem  44440  xlimclim  44540  icccncfext  44603  cncfiooicclem1  44609  itgsubsticclem  44691  ovolsplit  44704  dirkerval  44807  dirkercncflem4  44822  fourierdlem14  44837  fourierdlem15  44838  fourierdlem32  44855  fourierdlem33  44856  fourierdlem54  44876  fourierdlem62  44884  fourierdlem70  44892  fourierdlem81  44903  fourierdlem92  44914  fourierdlem102  44924  fourierdlem111  44933  fourierdlem114  44936  etransclem2  44952  rrxtopn0  45009  qndenserrnbllem  45010  qndenserrnbl  45011  qndenserrn  45015  rrnprjdstle  45017  ioorrnopnlem  45020  dmvolsal  45062  hoicvr  45264  hoissrrn  45265  hoiprodcl2  45271  hoicvrrex  45272  ovn0lem  45281  ovn02  45284  hsphoif  45292  hoidmvval  45293  hoissrrn2  45294  hsphoival  45295  hoidmvlelem3  45313  hoidmvle  45316  ovnhoilem1  45317  ovnhoilem2  45318  ovnhoi  45319  hspval  45325  ovnlecvr2  45326  ovncvr2  45327  hoidifhspval2  45331  hoiqssbl  45341  hspmbllem2  45343  hspmbl  45345  hoimbl  45347  opnvonmbllem2  45349  ovolval2lem  45359  ovolval2  45360  ovolval3  45363  ovolval4lem2  45366  ovolval5lem2  45369  ovnovollem1  45372  ovnovollem2  45373  ovnovollem3  45374  vonvolmbllem  45376  vonvolmbl  45377  vitali2  45410  issmflem  45443  incsmf  45458  decsmf  45483  nsssmfmbflem  45494  smfresal  45504  smfmullem4  45510  smf2id  45517  refdivpm  47230  elbigo2  47238  elbigof  47240  elbigodm  47241  elbigoimp  47242  elbigolo1  47243  prelrrx2  47399  rrx2xpref1o  47404  rrx2xpreen  47405  rrx2linesl  47429  line2  47438  line2x  47440  line2y  47441  amgmlemALT  47850