Theorem reex 11243

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11233	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11209	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5327	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150  ℝcr 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  reelprrecn  11244  negfi  12214  xrex  13026  limsuple  15510  limsuplt  15511  limsupbnd1  15514  rlim  15527  rlimf  15533  rlimss  15534  ello12  15548  lo1f  15550  lo1dm  15551  elo12  15559  o1f  15561  o1dm  15562  o1of2  15645  o1rlimmul  15651  o1add2  15656  o1mul2  15657  o1sub2  15658  o1dif  15662  caucvgrlem  15705  fsumo1  15844  rpnnen  16259  cpnnen  16261  ruclem13  16274  ruc  16275  aleph1re  16277  aleph1irr  16278  cnfldds  21393  cnflddsOLD  21406  replusg  21645  remulr  21646  rele2  21649  reds  21651  refldcj  21655  ismet  24348  tngngp2  24688  tngngpd  24689  tngngp  24690  tngngp3  24692  nrmtngnrm  24694  tngnrg  24710  rerest  24839  xrtgioo  24841  xrrest  24842  xrsmopn  24847  opnreen  24866  rectbntr0  24867  xrge0tsms  24869  bcthlem1  25371  bcthlem5  25375  reust  25428  rrxip  25437  rrx0el  25445  ehl0base  25463  ehl1eudis  25467  ehl2eudis  25469  pmltpclem2  25497  ovolficcss  25517  ovolval  25521  elovolmlem  25522  ovolctb2  25540  ismbl  25574  mblsplit  25580  voliunlem3  25600  dyadmbl  25648  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  vitalilem5  25660  vitali  25661  mbff  25673  ismbf  25676  ismbfcn  25677  mbfconst  25681  cncombf  25706  cnmbf  25707  0plef  25720  i1fd  25729  itg1ge0  25734  i1faddlem  25741  i1fmullem  25742  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulclem  25751  i1fmulc  25752  itg1mulc  25753  i1fsub  25757  itg1sub  25758  itg1lea  25761  itg1le  25762  mbfi1fseqlem2  25765  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1flimlem  25771  mbfmullem2  25773  itg2val  25777  xrge0f  25780  itg2ge0  25784  itg2itg1  25785  itg20  25786  itg2le  25788  itg2const  25789  itg2const2  25790  itg2seq  25791  itg2uba  25792  itg2lea  25793  itg2mulclem  25795  itg2mulc  25796  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  iblss  25854  i1fibl  25857  itgitg1  25858  itgle  25859  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgmulc2lem1  25881  bddmulibl  25888  bddiblnc  25891  dvnfre  26004  c1liplem1  26049  c1lip2  26051  lhop2  26068  dvcnvrelem2  26071  taylthlem2  26430  taylthlem2OLD  26431  dmarea  27014  vmadivsum  27540  rpvmasumlem  27545  mudivsum  27588  selberglem1  27603  selberglem2  27604  selberg2lem  27608  selberg2  27609  pntrsumo1  27623  selbergr  27626  iscgrgd  28535  elee  28923  xrge0tsmsd  33047  nn0omnd  33352  xrge0slmod  33355  raddcn  33889  rrhcn  33959  qqtopn  33973  dmvlsiga  34109  ddeval1  34214  ddeval0  34215  ddemeas  34216  mbfmcnt  34249  sxbrsigalem0  34252  sxbrsigalem3  34253  sxbrsigalem2  34267  isrrvv  34424  dstfrvclim1  34458  signsplypnf  34543  erdsze2lem1  35187  erdsze2lem2  35188  snmlval  35315  knoppcnlem5  36479  knoppcnlem6  36480  knoppcnlem7  36481  knoppcnlem8  36482  cnndvlem2  36520  icoreresf  37334  icoreval  37335  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimir  37639  broucube  37640  mblfinlem3  37645  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nclem1  37672  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  filbcmb  37726  rrncmslem  37818  repwsmet  37820  rrnequiv  37821  ismrer1  37824  absex  42267  pell1qrval  42833  pell14qrval  42835  pell1234qrval  42837  k0004ss1  44140  addrval  44461  subrval  44462  mulvval  44463  rpex  45295  climreeq  45568  limsupre  45596  limcresiooub  45597  limcresioolb  45598  limsuppnfdlem  45656  limsuppnflem  45665  limsupmnflem  45675  limsupre2lem  45679  xlimclim  45779  icccncfext  45842  cncfiooicclem1  45848  itgsubsticclem  45930  ovolsplit  45943  dirkerval  46046  dirkercncflem4  46061  fourierdlem14  46076  fourierdlem15  46077  fourierdlem32  46094  fourierdlem33  46095  fourierdlem54  46115  fourierdlem62  46123  fourierdlem70  46131  fourierdlem81  46142  fourierdlem92  46153  fourierdlem102  46163  fourierdlem111  46172  fourierdlem114  46175  etransclem2  46191  rrxtopn0  46248  qndenserrnbllem  46249  qndenserrnbl  46250  qndenserrn  46254  rrnprjdstle  46256  ioorrnopnlem  46259  dmvolsal  46301  hoicvr  46503  hoissrrn  46504  hoiprodcl2  46510  hoicvrrex  46511  ovn0lem  46520  ovn02  46523  hsphoif  46531  hoidmvval  46532  hoissrrn2  46533  hsphoival  46534  hoidmvlelem3  46552  hoidmvle  46555  ovnhoilem1  46556  ovnhoilem2  46557  ovnhoi  46558  hspval  46564  ovnlecvr2  46565  ovncvr2  46566  hoidifhspval2  46570  hoiqssbl  46580  hspmbllem2  46582  hspmbl  46584  hoimbl  46586  opnvonmbllem2  46588  ovolval2lem  46598  ovolval2  46599  ovolval3  46602  ovolval4lem2  46605  ovolval5lem2  46608  ovnovollem1  46611  ovnovollem2  46612  ovnovollem3  46613  vonvolmbllem  46615  vonvolmbl  46616  vitali2  46649  issmflem  46682  incsmf  46697  decsmf  46722  nsssmfmbflem  46733  smfresal  46743  smfmullem4  46749  smf2id  46756  refdivpm  48393  elbigo2  48401  elbigof  48403  elbigodm  48404  elbigoimp  48405  elbigolo1  48406  prelrrx2  48562  rrx2xpref1o  48567  rrx2xpreen  48568  rrx2linesl  48592  line2  48601  line2x  48603  line2y  48604  amgmlemALT  49033