Theorem reex 11129

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11119	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11095	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5263	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  ℝcr 11037

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 2708  ax-sep 5231  ax-cnex 11094  ax-resscn 11095

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  reelprrecn  11130  negfi  12105  xrex  12937  limsuple  15440  limsuplt  15441  limsupbnd1  15444  rlim  15457  rlimf  15463  rlimss  15464  ello12  15478  lo1f  15480  lo1dm  15481  elo12  15489  o1f  15491  o1dm  15492  o1of2  15575  o1rlimmul  15581  o1add2  15586  o1mul2  15587  o1sub2  15588  o1dif  15592  caucvgrlem  15635  fsumo1  15775  rpnnen  16194  cpnnen  16196  ruclem13  16209  ruc  16210  aleph1re  16212  aleph1irr  16213  cnfldds  21364  replusg  21590  remulr  21591  rele2  21594  reds  21596  refldcj  21600  ismet  24288  tngngp2  24617  tngngpd  24618  tngngp  24619  tngngp3  24621  nrmtngnrm  24623  tngnrg  24639  rerest  24769  xrtgioo  24772  xrrest  24773  xrsmopn  24778  opnreen  24797  rectbntr0  24798  xrge0tsms  24800  bcthlem1  25291  bcthlem5  25295  reust  25348  rrxip  25357  rrx0el  25365  ehl0base  25383  ehl1eudis  25387  ehl2eudis  25389  pmltpclem2  25416  ovolficcss  25436  ovolval  25440  elovolmlem  25441  ovolctb2  25459  ismbl  25493  mblsplit  25499  voliunlem3  25519  dyadmbl  25567  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  vitalilem5  25579  vitali  25580  mbff  25592  ismbf  25595  ismbfcn  25596  mbfconst  25600  cncombf  25625  cnmbf  25626  0plef  25639  i1fd  25648  itg1ge0  25653  i1faddlem  25660  i1fmullem  25661  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  i1fmulclem  25669  i1fmulc  25670  itg1mulc  25671  i1fsub  25675  itg1sub  25676  itg1lea  25679  itg1le  25680  mbfi1fseqlem2  25683  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1flimlem  25689  mbfmullem2  25691  itg2val  25695  xrge0f  25698  itg2ge0  25702  itg2itg1  25703  itg20  25704  itg2le  25706  itg2const  25707  itg2const2  25708  itg2seq  25709  itg2uba  25710  itg2lea  25711  itg2mulclem  25713  itg2mulc  25714  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  iblss  25772  i1fibl  25775  itgitg1  25776  itgle  25777  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  bddiblnc  25809  dvnfre  25919  c1liplem1  25963  c1lip2  25965  lhop2  25982  dvcnvrelem2  25985  taylthlem2  26339  dmarea  26921  vmadivsum  27445  rpvmasumlem  27450  mudivsum  27493  selberglem1  27508  selberglem2  27509  selberg2lem  27513  selberg2  27514  pntrsumo1  27528  selbergr  27531  iscgrgd  28581  elee  28962  xrge0tsmsd  33134  nn0omnd  33404  xrge0slmod  33408  raddcn  34073  rrhcn  34141  qqtopn  34155  dmvlsiga  34273  ddeval1  34378  ddeval0  34379  ddemeas  34380  mbfmcnt  34412  sxbrsigalem0  34415  sxbrsigalem3  34416  sxbrsigalem2  34430  isrrvv  34587  dstfrvclim1  34622  signsplypnf  34694  erdsze2lem1  35385  erdsze2lem2  35386  snmlval  35513  knoppcnlem5  36757  knoppcnlem6  36758  knoppcnlem7  36759  knoppcnlem8  36760  cnndvlem2  36798  icoreresf  37668  icoreval  37669  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimir  37974  broucube  37975  mblfinlem3  37980  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  itgmulc2nclem1  38007  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  filbcmb  38061  rrncmslem  38153  repwsmet  38155  rrnequiv  38156  ismrer1  38159  absex  42687  pell1qrval  43274  pell14qrval  43276  pell1234qrval  43278  k0004ss1  44578  addrval  44892  subrval  44893  mulvval  44894  rpex  45776  climreeq  46043  limsupre  46069  limcresiooub  46070  limcresioolb  46071  limsuppnfdlem  46129  limsuppnflem  46138  limsupmnflem  46148  limsupre2lem  46152  xlimclim  46252  icccncfext  46315  cncfiooicclem1  46321  itgsubsticclem  46403  ovolsplit  46416  dirkerval  46519  dirkercncflem4  46534  fourierdlem14  46549  fourierdlem15  46550  fourierdlem32  46567  fourierdlem33  46568  fourierdlem54  46588  fourierdlem62  46596  fourierdlem70  46604  fourierdlem81  46615  fourierdlem92  46626  fourierdlem102  46636  fourierdlem111  46645  fourierdlem114  46648  etransclem2  46664  rrxtopn0  46721  qndenserrnbllem  46722  qndenserrnbl  46723  qndenserrn  46727  rrnprjdstle  46729  ioorrnopnlem  46732  dmvolsal  46774  hoicvr  46976  hoissrrn  46977  hoiprodcl2  46983  hoicvrrex  46984  ovn0lem  46993  ovn02  46996  hsphoif  47004  hoidmvval  47005  hoissrrn2  47006  hsphoival  47007  hoidmvlelem3  47025  hoidmvle  47028  ovnhoilem1  47029  ovnhoilem2  47030  ovnhoi  47031  hspval  47037  ovnlecvr2  47038  ovncvr2  47039  hoidifhspval2  47043  hoiqssbl  47053  hspmbllem2  47055  hspmbl  47057  hoimbl  47059  opnvonmbllem2  47061  ovolval2lem  47071  ovolval2  47072  ovolval3  47075  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  ovnovollem2  47085  ovnovollem3  47086  vonvolmbllem  47088  vonvolmbl  47089  vitali2  47122  issmflem  47155  incsmf  47170  decsmf  47195  nsssmfmbflem  47206  smfresal  47216  smfmullem4  47222  smf2id  47229  nthrucw  47316  refdivpm  49020  elbigo2  49028  elbigof  49030  elbigodm  49031  elbigoimp  49032  elbigolo1  49033  prelrrx2  49189  rrx2xpref1o  49194  rrx2xpreen  49195  rrx2linesl  49219  line2  49228  line2x  49230  line2y  49231  amgmlemALT  50278