Theorem reex 11127

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11117	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11093	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5257	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3432  ℂcc 11034  ℝcr 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-cnex 11092  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  reelprrecn  11128  negfi  12103  xrex  12935  limsuple  15438  limsuplt  15439  limsupbnd1  15442  rlim  15455  rlimf  15461  rlimss  15462  ello12  15476  lo1f  15478  lo1dm  15479  elo12  15487  o1f  15489  o1dm  15490  o1of2  15573  o1rlimmul  15579  o1add2  15584  o1mul2  15585  o1sub2  15586  o1dif  15590  caucvgrlem  15633  fsumo1  15773  rpnnen  16192  cpnnen  16194  ruclem13  16207  ruc  16208  aleph1re  16210  aleph1irr  16211  cnfldds  21366  replusg  21592  remulr  21593  rele2  21596  reds  21598  refldcj  21602  ismet  24313  tngngp2  24642  tngngpd  24643  tngngp  24644  tngngp3  24646  nrmtngnrm  24648  tngnrg  24664  rerest  24794  xrtgioo  24797  xrrest  24798  xrsmopn  24803  opnreen  24822  rectbntr0  24823  xrge0tsms  24825  bcthlem1  25316  bcthlem5  25320  reust  25373  rrxip  25382  rrx0el  25390  ehl0base  25408  ehl1eudis  25412  ehl2eudis  25414  pmltpclem2  25441  ovolficcss  25461  ovolval  25465  elovolmlem  25466  ovolctb2  25484  ismbl  25518  mblsplit  25524  voliunlem3  25544  dyadmbl  25592  vitalilem2  25601  vitalilem3  25602  vitalilem4  25603  vitalilem5  25604  vitali  25605  mbff  25617  ismbf  25620  ismbfcn  25621  mbfconst  25625  cncombf  25650  cnmbf  25651  0plef  25664  i1fd  25673  itg1ge0  25678  i1faddlem  25685  i1fmullem  25686  i1fadd  25687  i1fmul  25688  itg1addlem4  25691  i1fmulclem  25694  i1fmulc  25695  itg1mulc  25696  i1fsub  25700  itg1sub  25701  itg1lea  25704  itg1le  25705  mbfi1fseqlem2  25708  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1flimlem  25714  mbfmullem2  25716  itg2val  25720  xrge0f  25723  itg2ge0  25727  itg2itg1  25728  itg20  25729  itg2le  25731  itg2const  25732  itg2const2  25733  itg2seq  25734  itg2uba  25735  itg2lea  25736  itg2mulclem  25738  itg2mulc  25739  itg2splitlem  25740  itg2split  25741  itg2monolem1  25742  itg2mono  25745  itg2i1fseqle  25746  itg2i1fseq  25747  itg2addlem  25750  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  iblss  25797  i1fibl  25800  itgitg1  25801  itgle  25802  ibladdlem  25812  itgaddlem1  25815  iblabslem  25820  iblabs  25821  iblabsr  25822  iblmulc2  25823  itgmulc2lem1  25824  bddmulibl  25831  bddiblnc  25834  dvnfre  25944  c1liplem1  25988  c1lip2  25990  lhop2  26007  dvcnvrelem2  26010  taylthlem2  26364  dmarea  26946  vmadivsum  27470  rpvmasumlem  27475  mudivsum  27518  selberglem1  27533  selberglem2  27534  selberg2lem  27538  selberg2  27539  pntrsumo1  27553  selbergr  27556  iscgrgd  28606  elee  28987  xrge0tsmsd  33161  nn0omnd  33434  xrge0slmod  33438  raddcn  34120  rrhcn  34188  qqtopn  34202  dmvlsiga  34320  ddeval1  34425  ddeval0  34426  ddemeas  34427  mbfmcnt  34459  sxbrsigalem0  34462  sxbrsigalem3  34463  sxbrsigalem2  34477  isrrvv  34634  dstfrvclim1  34669  signsplypnf  34741  erdsze2lem1  35438  erdsze2lem2  35439  snmlval  35566  knoppcnlem5  36810  knoppcnlem6  36811  knoppcnlem7  36812  knoppcnlem8  36813  cnndvlem2  36851  icoreresf  37721  icoreval  37722  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  poimir  38027  broucube  38028  mblfinlem3  38033  itg2addnclem  38045  itg2addnclem3  38047  itg2addnc  38048  itg2gt0cn  38049  ibladdnclem  38050  itgaddnclem1  38052  iblabsnclem  38057  iblabsnc  38058  iblmulc2nc  38059  itgmulc2nclem1  38060  ftc1anclem3  38069  ftc1anclem4  38070  ftc1anclem5  38071  ftc1anclem6  38072  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  filbcmb  38114  rrncmslem  38206  repwsmet  38208  rrnequiv  38209  ismrer1  38212  absex  42739  pell1qrval  43298  pell14qrval  43300  pell1234qrval  43302  k0004ss1  44602  addrval  44916  subrval  44917  mulvval  44918  rpex  45798  climreeq  46065  limsupre  46091  limcresiooub  46092  limcresioolb  46093  limsuppnfdlem  46151  limsuppnflem  46160  limsupmnflem  46170  limsupre2lem  46174  xlimclim  46274  icccncfext  46337  cncfiooicclem1  46343  itgsubsticclem  46425  ovolsplit  46438  dirkerval  46541  dirkercncflem4  46556  fourierdlem14  46571  fourierdlem15  46572  fourierdlem32  46589  fourierdlem33  46590  fourierdlem54  46610  fourierdlem62  46618  fourierdlem70  46626  fourierdlem81  46637  fourierdlem92  46648  fourierdlem102  46658  fourierdlem111  46667  fourierdlem114  46670  etransclem2  46686  rrxtopn0  46743  qndenserrnbllem  46744  qndenserrnbl  46745  qndenserrn  46749  rrnprjdstle  46751  ioorrnopnlem  46754  dmvolsal  46796  hoicvr  46998  hoissrrn  46999  hoiprodcl2  47005  hoicvrrex  47006  ovn0lem  47015  ovn02  47018  hsphoif  47026  hoidmvval  47027  hoissrrn2  47028  hsphoival  47029  hoidmvlelem3  47047  hoidmvle  47050  ovnhoilem1  47051  ovnhoilem2  47052  ovnhoi  47053  hspval  47059  ovnlecvr2  47060  ovncvr2  47061  hoidifhspval2  47065  hoiqssbl  47075  hspmbllem2  47077  hspmbl  47079  hoimbl  47081  opnvonmbllem2  47083  ovolval2lem  47093  ovolval2  47094  ovolval3  47097  ovolval4lem2  47100  ovolval5lem2  47103  ovnovollem1  47106  ovnovollem2  47107  ovnovollem3  47108  vonvolmbllem  47110  vonvolmbl  47111  vitali2  47144  issmflem  47177  incsmf  47192  decsmf  47217  nsssmfmbflem  47228  smfresal  47238  smfmullem4  47244  smf2id  47251  nthrucw  47338  refdivpm  49042  elbigo2  49050  elbigof  49052  elbigodm  49053  elbigoimp  49054  elbigolo1  49055  prelrrx2  49211  rrx2xpref1o  49216  rrx2xpreen  49217  rrx2linesl  49241  line2  49250  line2x  49252  line2y  49253  amgmlemALT  50300