Theorem reex 11129

Description: The real numbers form a set. See also reexALT 12909. (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 5269	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂ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 2709  ax-sep 5243  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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  reelprrecn  11130  negfi  12103  xrex  12912  limsuple  15413  limsuplt  15414  limsupbnd1  15417  rlim  15430  rlimf  15436  rlimss  15437  ello12  15451  lo1f  15453  lo1dm  15454  elo12  15462  o1f  15464  o1dm  15465  o1of2  15548  o1rlimmul  15554  o1add2  15559  o1mul2  15560  o1sub2  15561  o1dif  15565  caucvgrlem  15608  fsumo1  15747  rpnnen  16164  cpnnen  16166  ruclem13  16179  ruc  16180  aleph1re  16182  aleph1irr  16183  cnfldds  21333  cnflddsOLD  21346  replusg  21577  remulr  21578  rele2  21581  reds  21583  refldcj  21587  ismet  24279  tngngp2  24608  tngngpd  24609  tngngp  24610  tngngp3  24612  nrmtngnrm  24614  tngnrg  24630  rerest  24760  xrtgioo  24763  xrrest  24764  xrsmopn  24769  opnreen  24788  rectbntr0  24789  xrge0tsms  24791  bcthlem1  25292  bcthlem5  25296  reust  25349  rrxip  25358  rrx0el  25366  ehl0base  25384  ehl1eudis  25388  ehl2eudis  25390  pmltpclem2  25418  ovolficcss  25438  ovolval  25442  elovolmlem  25443  ovolctb2  25461  ismbl  25495  mblsplit  25501  voliunlem3  25521  dyadmbl  25569  vitalilem2  25578  vitalilem3  25579  vitalilem4  25580  vitalilem5  25581  vitali  25582  mbff  25594  ismbf  25597  ismbfcn  25598  mbfconst  25602  cncombf  25627  cnmbf  25628  0plef  25641  i1fd  25650  itg1ge0  25655  i1faddlem  25662  i1fmullem  25663  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  i1fmulclem  25671  i1fmulc  25672  itg1mulc  25673  i1fsub  25677  itg1sub  25678  itg1lea  25681  itg1le  25682  mbfi1fseqlem2  25685  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1flimlem  25691  mbfmullem2  25693  itg2val  25697  xrge0f  25700  itg2ge0  25704  itg2itg1  25705  itg20  25706  itg2le  25708  itg2const  25709  itg2const2  25710  itg2seq  25711  itg2uba  25712  itg2lea  25713  itg2mulclem  25715  itg2mulc  25716  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2addlem  25727  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  iblss  25774  i1fibl  25777  itgitg1  25778  itgle  25779  ibladdlem  25789  itgaddlem1  25792  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  bddiblnc  25811  dvnfre  25924  c1liplem1  25969  c1lip2  25971  lhop2  25988  dvcnvrelem2  25991  taylthlem2  26350  taylthlem2OLD  26351  dmarea  26935  vmadivsum  27461  rpvmasumlem  27466  mudivsum  27509  selberglem1  27524  selberglem2  27525  selberg2lem  27529  selberg2  27530  pntrsumo1  27544  selbergr  27547  iscgrgd  28597  elee  28978  xrge0tsmsd  33166  nn0omnd  33436  xrge0slmod  33440  raddcn  34106  rrhcn  34174  qqtopn  34188  dmvlsiga  34306  ddeval1  34411  ddeval0  34412  ddemeas  34413  mbfmcnt  34445  sxbrsigalem0  34448  sxbrsigalem3  34449  sxbrsigalem2  34463  isrrvv  34620  dstfrvclim1  34655  signsplypnf  34727  erdsze2lem1  35416  erdsze2lem2  35417  snmlval  35544  knoppcnlem5  36716  knoppcnlem6  36717  knoppcnlem7  36718  knoppcnlem8  36719  cnndvlem2  36757  icoreresf  37604  icoreval  37605  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  poimir  37901  broucube  37902  mblfinlem3  37907  itg2addnclem  37919  itg2addnclem3  37921  itg2addnc  37922  itg2gt0cn  37923  ibladdnclem  37924  itgaddnclem1  37926  iblabsnclem  37931  iblabsnc  37932  iblmulc2nc  37933  itgmulc2nclem1  37934  ftc1anclem3  37943  ftc1anclem4  37944  ftc1anclem5  37945  ftc1anclem6  37946  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  filbcmb  37988  rrncmslem  38080  repwsmet  38082  rrnequiv  38083  ismrer1  38086  absex  42615  pell1qrval  43200  pell14qrval  43202  pell1234qrval  43204  k0004ss1  44504  addrval  44818  subrval  44819  mulvval  44820  rpex  45702  climreeq  45970  limsupre  45996  limcresiooub  45997  limcresioolb  45998  limsuppnfdlem  46056  limsuppnflem  46065  limsupmnflem  46075  limsupre2lem  46079  xlimclim  46179  icccncfext  46242  cncfiooicclem1  46248  itgsubsticclem  46330  ovolsplit  46343  dirkerval  46446  dirkercncflem4  46461  fourierdlem14  46476  fourierdlem15  46477  fourierdlem32  46494  fourierdlem33  46495  fourierdlem54  46515  fourierdlem62  46523  fourierdlem70  46531  fourierdlem81  46542  fourierdlem92  46553  fourierdlem102  46563  fourierdlem111  46572  fourierdlem114  46575  etransclem2  46591  rrxtopn0  46648  qndenserrnbllem  46649  qndenserrnbl  46650  qndenserrn  46654  rrnprjdstle  46656  ioorrnopnlem  46659  dmvolsal  46701  hoicvr  46903  hoissrrn  46904  hoiprodcl2  46910  hoicvrrex  46911  ovn0lem  46920  ovn02  46923  hsphoif  46931  hoidmvval  46932  hoissrrn2  46933  hsphoival  46934  hoidmvlelem3  46952  hoidmvle  46955  ovnhoilem1  46956  ovnhoilem2  46957  ovnhoi  46958  hspval  46964  ovnlecvr2  46965  ovncvr2  46966  hoidifhspval2  46970  hoiqssbl  46980  hspmbllem2  46982  hspmbl  46984  hoimbl  46986  opnvonmbllem2  46988  ovolval2lem  46998  ovolval2  46999  ovolval3  47002  ovolval4lem2  47005  ovolval5lem2  47008  ovnovollem1  47011  ovnovollem2  47012  ovnovollem3  47013  vonvolmbllem  47015  vonvolmbl  47016  vitali2  47049  issmflem  47082  incsmf  47097  decsmf  47122  nsssmfmbflem  47133  smfresal  47143  smfmullem4  47149  smf2id  47156  nthrucw  47241  refdivpm  48901  elbigo2  48909  elbigof  48911  elbigodm  48912  elbigoimp  48913  elbigolo1  48914  prelrrx2  49070  rrx2xpref1o  49075  rrx2xpreen  49076  rrx2linesl  49100  line2  49109  line2x  49111  line2y  49112  amgmlemALT  50159