Theorem reex 9906

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 9896	. 2 ⊢ ℂ ∈ V
2		ax-resscn 9872	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 4731	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ℂcc 9813  ℝcr 9814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-cnex 9871  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  reelprrecn  9907  negfi  10850  xrex  11705  limsuple  14057  limsuplt  14058  limsupbnd1  14061  rlim  14074  rlimf  14080  rlimss  14081  ello12  14095  lo1f  14097  lo1dm  14098  elo12  14106  o1f  14108  o1dm  14109  o1of2  14191  o1rlimmul  14197  o1add2  14202  o1mul2  14203  o1sub2  14204  o1dif  14208  caucvgrlem  14251  fsumo1  14385  rpnnen  14795  cpnnen  14797  ruclem13  14810  ruc  14811  aleph1re  14813  aleph1irr  14814  cnfldds  19577  replusg  19775  remulr  19776  rele2  19779  reds  19781  refldcj  19785  ismet  21938  tngngp2  22266  tngngpd  22267  tngngp  22268  tngngp3  22270  nrmtngnrm  22272  tngnrg  22288  rerest  22415  xrtgioo  22417  xrrest  22418  xrsmopn  22423  opnreen  22442  rectbntr0  22443  xrge0tsms  22445  bcthlem1  22929  bcthlem5  22933  reust  22977  rrxip  22986  pmltpclem2  23025  ovolficcss  23045  ovolval  23049  elovolm  23050  elovolmr  23051  ovolmge0  23052  ovolgelb  23055  ovolctb2  23067  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovolshftlem2  23085  ovolicc2  23097  ismbl  23101  mblsplit  23107  voliunlem3  23127  ioombl1  23137  dyadmbl  23174  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  vitalilem5  23187  vitali  23188  mbff  23200  ismbf  23203  ismbfcn  23204  mbfconst  23208  cncombf  23231  cnmbf  23232  0plef  23245  i1fd  23254  itg1ge0  23259  i1faddlem  23266  i1fmullem  23267  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulclem  23275  i1fmulc  23276  itg1mulc  23277  i1fsub  23281  itg1sub  23282  itg1lea  23285  itg1le  23286  mbfi1fseqlem2  23289  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1flimlem  23295  mbfmullem2  23297  itg2val  23301  xrge0f  23304  itg2ge0  23308  itg2itg1  23309  itg20  23310  itg2le  23312  itg2const  23313  itg2const2  23314  itg2seq  23315  itg2uba  23316  itg2lea  23317  itg2mulclem  23319  itg2mulc  23320  itg2splitlem  23321  itg2split  23322  itg2monolem1  23323  itg2mono  23326  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  iblss  23377  i1fibl  23380  itgitg1  23381  itgle  23382  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2lem1  23404  bddmulibl  23411  dvnfre  23521  c1liplem1  23563  c1lip2  23565  lhop2  23582  dvcnvrelem2  23585  taylthlem2  23932  dmarea  24484  vmadivsum  24971  rpvmasumlem  24976  mudivsum  25019  selberglem1  25034  selberglem2  25035  selberg2lem  25039  selberg2  25040  pntrsumo1  25054  selbergr  25057  iscgrgd  25208  elee  25574  xrge0tsmsd  29116  nn0omnd  29172  xrge0slmod  29175  raddcn  29303  rrhcn  29369  qqtopn  29383  dmvlsiga  29519  ddeval1  29624  ddeval0  29625  ddemeas  29626  mbfmcnt  29657  sxbrsigalem0  29660  sxbrsigalem3  29661  sxbrsigalem2  29675  isrrvv  29832  dstfrvclim1  29866  signsplypnf  29953  erdsze2lem1  30439  erdsze2lem2  30440  snmlval  30567  knoppcnlem5  31657  knoppcnlem6  31658  knoppcnlem7  31659  knoppcnlem8  31660  cnndvlem2  31699  icoreresf  32376  icoreval  32377  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimir  32612  broucube  32613  mblfinlem3  32618  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nclem1  32646  bddiblnc  32650  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  filbcmb  32705  rrncmslem  32801  repwsmet  32803  rrnequiv  32804  ismrer1  32807  pell1qrval  36428  pell14qrval  36430  pell1234qrval  36432  k0004ss1  37469  addrval  37691  subrval  37692  mulvval  37693  climreeq  38680  limsupre  38708  limcresiooub  38709  limcresioolb  38710  icccncfext  38773  cncfiooicclem1  38779  itgsubsticclem  38867  ovolsplit  38881  dirkerval  38984  dirkercncflem4  38999  fourierdlem14  39014  fourierdlem15  39015  fourierdlem32  39032  fourierdlem33  39033  fourierdlem54  39053  fourierdlem62  39061  fourierdlem70  39069  fourierdlem81  39080  fourierdlem92  39091  fourierdlem102  39101  fourierdlem111  39110  fourierdlem114  39113  etransclem2  39129  rrxtopn0  39189  qndenserrnbllem  39190  qndenserrnbl  39191  qndenserrn  39195  rrnprjdstle  39197  ioorrnopnlem  39200  dmvolsal  39240  hoicvr  39438  hoissrrn  39439  hoiprodcl2  39445  hoicvrrex  39446  ovn0lem  39455  ovn02  39458  hsphoif  39466  hoidmvval  39467  hoissrrn2  39468  hsphoival  39469  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem1  39491  ovnhoilem2  39492  ovnhoi  39493  hspval  39499  ovnlecvr2  39500  ovncvr2  39501  hoidifhspval2  39505  hoiqssbl  39515  hspmbllem2  39517  hspmbl  39519  hoimbl  39521  opnvonmbllem2  39523  ovolval2lem  39533  ovolval2  39534  ovolval3  39537  ovolval4lem2  39540  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  ovnovollem3  39548  vonvolmbllem  39550  vonvolmbl  39551  vitali2  39585  issmflem  39613  incsmf  39629  decsmf  39653  nsssmfmbflem  39664  smfresal  39673  smfmullem4  39679  smf2id  39686  refdivpm  42136  elbigo2  42144  elbigof  42146  elbigodm  42147  elbigoimp  42148  elbigolo1  42149  amgmlemALT  42358