Theorem reex 11159

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11149	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11125	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5277	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066  ℝcr 11067

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 5251  ax-cnex 11124  ax-resscn 11125

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 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  reelprrecn  11160  negfi  12132  xrex  12946  limsuple  15444  limsuplt  15445  limsupbnd1  15448  rlim  15461  rlimf  15467  rlimss  15468  ello12  15482  lo1f  15484  lo1dm  15485  elo12  15493  o1f  15495  o1dm  15496  o1of2  15579  o1rlimmul  15585  o1add2  15590  o1mul2  15591  o1sub2  15592  o1dif  15596  caucvgrlem  15639  fsumo1  15778  rpnnen  16195  cpnnen  16197  ruclem13  16210  ruc  16211  aleph1re  16213  aleph1irr  16214  cnfldds  21276  cnflddsOLD  21289  replusg  21519  remulr  21520  rele2  21523  reds  21525  refldcj  21529  ismet  24211  tngngp2  24540  tngngpd  24541  tngngp  24542  tngngp3  24544  nrmtngnrm  24546  tngnrg  24562  rerest  24692  xrtgioo  24695  xrrest  24696  xrsmopn  24701  opnreen  24720  rectbntr0  24721  xrge0tsms  24723  bcthlem1  25224  bcthlem5  25228  reust  25281  rrxip  25290  rrx0el  25298  ehl0base  25316  ehl1eudis  25320  ehl2eudis  25322  pmltpclem2  25350  ovolficcss  25370  ovolval  25374  elovolmlem  25375  ovolctb2  25393  ismbl  25427  mblsplit  25433  voliunlem3  25453  dyadmbl  25501  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  vitalilem5  25513  vitali  25514  mbff  25526  ismbf  25529  ismbfcn  25530  mbfconst  25534  cncombf  25559  cnmbf  25560  0plef  25573  i1fd  25582  itg1ge0  25587  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  i1fmulclem  25603  i1fmulc  25604  itg1mulc  25605  i1fsub  25609  itg1sub  25610  itg1lea  25613  itg1le  25614  mbfi1fseqlem2  25617  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1flimlem  25623  mbfmullem2  25625  itg2val  25629  xrge0f  25632  itg2ge0  25636  itg2itg1  25637  itg20  25638  itg2le  25640  itg2const  25641  itg2const2  25642  itg2seq  25643  itg2uba  25644  itg2lea  25645  itg2mulclem  25647  itg2mulc  25648  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2mono  25654  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  i1fibl  25709  itgitg1  25710  itgle  25711  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgmulc2lem1  25733  bddmulibl  25740  bddiblnc  25743  dvnfre  25856  c1liplem1  25901  c1lip2  25903  lhop2  25920  dvcnvrelem2  25923  taylthlem2  26282  taylthlem2OLD  26283  dmarea  26867  vmadivsum  27393  rpvmasumlem  27398  mudivsum  27441  selberglem1  27456  selberglem2  27457  selberg2lem  27461  selberg2  27462  pntrsumo1  27476  selbergr  27479  iscgrgd  28440  elee  28821  xrge0tsmsd  33002  nn0omnd  33316  xrge0slmod  33319  raddcn  33919  rrhcn  33987  qqtopn  34001  dmvlsiga  34119  ddeval1  34224  ddeval0  34225  ddemeas  34226  mbfmcnt  34259  sxbrsigalem0  34262  sxbrsigalem3  34263  sxbrsigalem2  34277  isrrvv  34434  dstfrvclim1  34469  signsplypnf  34541  erdsze2lem1  35190  erdsze2lem2  35191  snmlval  35318  knoppcnlem5  36485  knoppcnlem6  36486  knoppcnlem7  36487  knoppcnlem8  36488  cnndvlem2  36526  icoreresf  37340  icoreval  37341  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimir  37647  broucube  37648  mblfinlem3  37653  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nclem1  37680  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  filbcmb  37734  rrncmslem  37826  repwsmet  37828  rrnequiv  37829  ismrer1  37832  absex  42236  pell1qrval  42834  pell14qrval  42836  pell1234qrval  42838  k0004ss1  44140  addrval  44455  subrval  44456  mulvval  44457  rpex  45342  climreeq  45611  limsupre  45639  limcresiooub  45640  limcresioolb  45641  limsuppnfdlem  45699  limsuppnflem  45708  limsupmnflem  45718  limsupre2lem  45722  xlimclim  45822  icccncfext  45885  cncfiooicclem1  45891  itgsubsticclem  45973  ovolsplit  45986  dirkerval  46089  dirkercncflem4  46104  fourierdlem14  46119  fourierdlem15  46120  fourierdlem32  46137  fourierdlem33  46138  fourierdlem54  46158  fourierdlem62  46166  fourierdlem70  46174  fourierdlem81  46185  fourierdlem92  46196  fourierdlem102  46206  fourierdlem111  46215  fourierdlem114  46218  etransclem2  46234  rrxtopn0  46291  qndenserrnbllem  46292  qndenserrnbl  46293  qndenserrn  46297  rrnprjdstle  46299  ioorrnopnlem  46302  dmvolsal  46344  hoicvr  46546  hoissrrn  46547  hoiprodcl2  46553  hoicvrrex  46554  ovn0lem  46563  ovn02  46566  hsphoif  46574  hoidmvval  46575  hoissrrn2  46576  hsphoival  46577  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem1  46599  ovnhoilem2  46600  ovnhoi  46601  hspval  46607  ovnlecvr2  46608  ovncvr2  46609  hoidifhspval2  46613  hoiqssbl  46623  hspmbllem2  46625  hspmbl  46627  hoimbl  46629  opnvonmbllem2  46631  ovolval2lem  46641  ovolval2  46642  ovolval3  46645  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  ovnovollem3  46656  vonvolmbllem  46658  vonvolmbl  46659  vitali2  46692  issmflem  46725  incsmf  46740  decsmf  46765  nsssmfmbflem  46776  smfresal  46786  smfmullem4  46792  smf2id  46799  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