Theorem reex 11119

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11109	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11085	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5264	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ℂcc 11026  ℝcr 11027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  reelprrecn  11120  negfi  12092  xrex  12906  limsuple  15403  limsuplt  15404  limsupbnd1  15407  rlim  15420  rlimf  15426  rlimss  15427  ello12  15441  lo1f  15443  lo1dm  15444  elo12  15452  o1f  15454  o1dm  15455  o1of2  15538  o1rlimmul  15544  o1add2  15549  o1mul2  15550  o1sub2  15551  o1dif  15555  caucvgrlem  15598  fsumo1  15737  rpnnen  16154  cpnnen  16156  ruclem13  16169  ruc  16170  aleph1re  16172  aleph1irr  16173  cnfldds  21291  cnflddsOLD  21304  replusg  21535  remulr  21536  rele2  21539  reds  21541  refldcj  21545  ismet  24227  tngngp2  24556  tngngpd  24557  tngngp  24558  tngngp3  24560  nrmtngnrm  24562  tngnrg  24578  rerest  24708  xrtgioo  24711  xrrest  24712  xrsmopn  24717  opnreen  24736  rectbntr0  24737  xrge0tsms  24739  bcthlem1  25240  bcthlem5  25244  reust  25297  rrxip  25306  rrx0el  25314  ehl0base  25332  ehl1eudis  25336  ehl2eudis  25338  pmltpclem2  25366  ovolficcss  25386  ovolval  25390  elovolmlem  25391  ovolctb2  25409  ismbl  25443  mblsplit  25449  voliunlem3  25469  dyadmbl  25517  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  vitalilem5  25529  vitali  25530  mbff  25542  ismbf  25545  ismbfcn  25546  mbfconst  25550  cncombf  25575  cnmbf  25576  0plef  25589  i1fd  25598  itg1ge0  25603  i1faddlem  25610  i1fmullem  25611  i1fadd  25612  i1fmul  25613  itg1addlem4  25616  i1fmulclem  25619  i1fmulc  25620  itg1mulc  25621  i1fsub  25625  itg1sub  25626  itg1lea  25629  itg1le  25630  mbfi1fseqlem2  25633  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1flimlem  25639  mbfmullem2  25641  itg2val  25645  xrge0f  25648  itg2ge0  25652  itg2itg1  25653  itg20  25654  itg2le  25656  itg2const  25657  itg2const2  25658  itg2seq  25659  itg2uba  25660  itg2lea  25661  itg2mulclem  25663  itg2mulc  25664  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2mono  25670  itg2i1fseqle  25671  itg2i1fseq  25672  itg2addlem  25675  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  i1fibl  25725  itgitg1  25726  itgle  25727  ibladdlem  25737  itgaddlem1  25740  iblabslem  25745  iblabs  25746  iblabsr  25747  iblmulc2  25748  itgmulc2lem1  25749  bddmulibl  25756  bddiblnc  25759  dvnfre  25872  c1liplem1  25917  c1lip2  25919  lhop2  25936  dvcnvrelem2  25939  taylthlem2  26298  taylthlem2OLD  26299  dmarea  26883  vmadivsum  27409  rpvmasumlem  27414  mudivsum  27457  selberglem1  27472  selberglem2  27473  selberg2lem  27477  selberg2  27478  pntrsumo1  27492  selbergr  27495  iscgrgd  28476  elee  28857  xrge0tsmsd  33028  nn0omnd  33295  xrge0slmod  33298  raddcn  33898  rrhcn  33966  qqtopn  33980  dmvlsiga  34098  ddeval1  34203  ddeval0  34204  ddemeas  34205  mbfmcnt  34238  sxbrsigalem0  34241  sxbrsigalem3  34242  sxbrsigalem2  34256  isrrvv  34413  dstfrvclim1  34448  signsplypnf  34520  erdsze2lem1  35178  erdsze2lem2  35179  snmlval  35306  knoppcnlem5  36473  knoppcnlem6  36474  knoppcnlem7  36475  knoppcnlem8  36476  cnndvlem2  36514  icoreresf  37328  icoreval  37329  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimir  37635  broucube  37636  mblfinlem3  37641  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  itg2gt0cn  37657  ibladdnclem  37658  itgaddnclem1  37660  iblabsnclem  37665  iblabsnc  37666  iblmulc2nc  37667  itgmulc2nclem1  37668  ftc1anclem3  37677  ftc1anclem4  37678  ftc1anclem5  37679  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  filbcmb  37722  rrncmslem  37814  repwsmet  37816  rrnequiv  37817  ismrer1  37820  absex  42224  pell1qrval  42822  pell14qrval  42824  pell1234qrval  42826  k0004ss1  44127  addrval  44442  subrval  44443  mulvval  44444  rpex  45329  climreeq  45598  limsupre  45626  limcresiooub  45627  limcresioolb  45628  limsuppnfdlem  45686  limsuppnflem  45695  limsupmnflem  45705  limsupre2lem  45709  xlimclim  45809  icccncfext  45872  cncfiooicclem1  45878  itgsubsticclem  45960  ovolsplit  45973  dirkerval  46076  dirkercncflem4  46091  fourierdlem14  46106  fourierdlem15  46107  fourierdlem32  46124  fourierdlem33  46125  fourierdlem54  46145  fourierdlem62  46153  fourierdlem70  46161  fourierdlem81  46172  fourierdlem92  46183  fourierdlem102  46193  fourierdlem111  46202  fourierdlem114  46205  etransclem2  46221  rrxtopn0  46278  qndenserrnbllem  46279  qndenserrnbl  46280  qndenserrn  46284  rrnprjdstle  46286  ioorrnopnlem  46289  dmvolsal  46331  hoicvr  46533  hoissrrn  46534  hoiprodcl2  46540  hoicvrrex  46541  ovn0lem  46550  ovn02  46553  hsphoif  46561  hoidmvval  46562  hoissrrn2  46563  hsphoival  46564  hoidmvlelem3  46582  hoidmvle  46585  ovnhoilem1  46586  ovnhoilem2  46587  ovnhoi  46588  hspval  46594  ovnlecvr2  46595  ovncvr2  46596  hoidifhspval2  46600  hoiqssbl  46610  hspmbllem2  46612  hspmbl  46614  hoimbl  46616  opnvonmbllem2  46618  ovolval2lem  46628  ovolval2  46629  ovolval3  46632  ovolval4lem2  46635  ovolval5lem2  46638  ovnovollem1  46641  ovnovollem2  46642  ovnovollem3  46643  vonvolmbllem  46645  vonvolmbl  46646  vitali2  46679  issmflem  46712  incsmf  46727  decsmf  46752  nsssmfmbflem  46763  smfresal  46773  smfmullem4  46779  smf2id  46786  refdivpm  48533  elbigo2  48541  elbigof  48543  elbigodm  48544  elbigoimp  48545  elbigolo1  48546  prelrrx2  48702  rrx2xpref1o  48707  rrx2xpreen  48708  rrx2linesl  48732  line2  48741  line2x  48743  line2y  48744  amgmlemALT  49792