MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reex Structured version   Visualization version   GIF version

Theorem reex 9987
Description: The real numbers form a set. See also reexALT 11786. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
reex ℝ ∈ V

Proof of Theorem reex
StepHypRef Expression
1 cnex 9977 . 2 ℂ ∈ V
2 ax-resscn 9953 . 2 ℝ ⊆ ℂ
31, 2ssexi 4773 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3190  cc 9894  cr 9895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-cnex 9952  ax-resscn 9953
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567  df-ss 3574
This theorem is referenced by:  reelprrecn  9988  negfi  10931  xrex  11789  limsuple  14159  limsuplt  14160  limsupbnd1  14163  rlim  14176  rlimf  14182  rlimss  14183  ello12  14197  lo1f  14199  lo1dm  14200  elo12  14208  o1f  14210  o1dm  14211  o1of2  14293  o1rlimmul  14299  o1add2  14304  o1mul2  14305  o1sub2  14306  o1dif  14310  caucvgrlem  14353  fsumo1  14490  rpnnen  14900  cpnnen  14902  ruclem13  14915  ruc  14916  aleph1re  14918  aleph1irr  14919  cnfldds  19696  replusg  19896  remulr  19897  rele2  19900  reds  19902  refldcj  19906  ismet  22068  tngngp2  22396  tngngpd  22397  tngngp  22398  tngngp3  22400  nrmtngnrm  22402  tngnrg  22418  rerest  22547  xrtgioo  22549  xrrest  22550  xrsmopn  22555  opnreen  22574  rectbntr0  22575  xrge0tsms  22577  bcthlem1  23061  bcthlem5  23065  reust  23109  rrxip  23118  pmltpclem2  23158  ovolficcss  23178  ovolval  23182  elovolm  23183  elovolmr  23184  ovolmge0  23185  ovolgelb  23188  ovolctb2  23200  ovolunlem1a  23204  ovolunlem1  23205  ovoliunlem1  23210  ovoliunlem2  23211  ovolshftlem2  23218  ovolicc2  23230  ismbl  23234  mblsplit  23240  voliunlem3  23260  ioombl1  23270  dyadmbl  23308  vitalilem2  23318  vitalilem3  23319  vitalilem4  23320  vitalilem5  23321  vitali  23322  mbff  23334  ismbf  23337  ismbfcn  23338  mbfconst  23342  cncombf  23365  cnmbf  23366  0plef  23379  i1fd  23388  itg1ge0  23393  i1faddlem  23400  i1fmullem  23401  i1fadd  23402  i1fmul  23403  itg1addlem4  23406  i1fmulclem  23409  i1fmulc  23410  itg1mulc  23411  i1fsub  23415  itg1sub  23416  itg1lea  23419  itg1le  23420  mbfi1fseqlem2  23423  mbfi1fseqlem4  23425  mbfi1fseqlem5  23426  mbfi1flimlem  23429  mbfmullem2  23431  itg2val  23435  xrge0f  23438  itg2ge0  23442  itg2itg1  23443  itg20  23444  itg2le  23446  itg2const  23447  itg2const2  23448  itg2seq  23449  itg2uba  23450  itg2lea  23451  itg2mulclem  23453  itg2mulc  23454  itg2splitlem  23455  itg2split  23456  itg2monolem1  23457  itg2mono  23460  itg2i1fseqle  23461  itg2i1fseq  23462  itg2addlem  23465  itg2gt0  23467  itg2cnlem1  23468  itg2cnlem2  23469  iblss  23511  i1fibl  23514  itgitg1  23515  itgle  23516  ibladdlem  23526  itgaddlem1  23529  iblabslem  23534  iblabs  23535  iblabsr  23536  iblmulc2  23537  itgmulc2lem1  23538  bddmulibl  23545  dvnfre  23655  c1liplem1  23697  c1lip2  23699  lhop2  23716  dvcnvrelem2  23719  taylthlem2  24066  dmarea  24618  vmadivsum  25105  rpvmasumlem  25110  mudivsum  25153  selberglem1  25168  selberglem2  25169  selberg2lem  25173  selberg2  25174  pntrsumo1  25188  selbergr  25191  iscgrgd  25342  elee  25708  xrge0tsmsd  29612  nn0omnd  29668  xrge0slmod  29671  raddcn  29799  rrhcn  29865  qqtopn  29879  dmvlsiga  30015  ddeval1  30120  ddeval0  30121  ddemeas  30122  mbfmcnt  30153  sxbrsigalem0  30156  sxbrsigalem3  30157  sxbrsigalem2  30171  isrrvv  30328  dstfrvclim1  30362  signsplypnf  30449  erdsze2lem1  30946  erdsze2lem2  30947  snmlval  31074  knoppcnlem5  32182  knoppcnlem6  32183  knoppcnlem7  32184  knoppcnlem8  32185  cnndvlem2  32224  icoreresf  32871  icoreval  32872  poimirlem29  33109  poimirlem30  33110  poimirlem31  33111  poimir  33113  broucube  33114  mblfinlem3  33119  itg2addnclem  33132  itg2addnclem3  33134  itg2addnc  33135  itg2gt0cn  33136  ibladdnclem  33137  itgaddnclem1  33139  iblabsnclem  33144  iblabsnc  33145  iblmulc2nc  33146  itgmulc2nclem1  33147  bddiblnc  33151  ftc1anclem3  33158  ftc1anclem4  33159  ftc1anclem5  33160  ftc1anclem6  33161  ftc1anclem7  33162  ftc1anclem8  33163  ftc1anc  33164  filbcmb  33206  rrncmslem  33302  repwsmet  33304  rrnequiv  33305  ismrer1  33308  pell1qrval  36929  pell14qrval  36931  pell1234qrval  36933  k0004ss1  37970  addrval  38191  subrval  38192  mulvval  38193  climreeq  39281  limsupre  39309  limcresiooub  39310  limcresioolb  39311  limsuppnfdlem  39369  limsuppnflem  39378  limsupmnflem  39388  limsupre2lem  39392  icccncfext  39435  cncfiooicclem1  39441  itgsubsticclem  39528  ovolsplit  39542  dirkerval  39645  dirkercncflem4  39660  fourierdlem14  39675  fourierdlem15  39676  fourierdlem32  39693  fourierdlem33  39694  fourierdlem54  39714  fourierdlem62  39722  fourierdlem70  39730  fourierdlem81  39741  fourierdlem92  39752  fourierdlem102  39762  fourierdlem111  39771  fourierdlem114  39774  etransclem2  39790  rrxtopn0  39850  qndenserrnbllem  39851  qndenserrnbl  39852  qndenserrn  39856  rrnprjdstle  39858  ioorrnopnlem  39861  dmvolsal  39901  hoicvr  40099  hoissrrn  40100  hoiprodcl2  40106  hoicvrrex  40107  ovn0lem  40116  ovn02  40119  hsphoif  40127  hoidmvval  40128  hoissrrn2  40129  hsphoival  40130  hoidmvlelem3  40148  hoidmvle  40151  ovnhoilem1  40152  ovnhoilem2  40153  ovnhoi  40154  hspval  40160  ovnlecvr2  40161  ovncvr2  40162  hoidifhspval2  40166  hoiqssbl  40176  hspmbllem2  40178  hspmbl  40180  hoimbl  40182  opnvonmbllem2  40184  ovolval2lem  40194  ovolval2  40195  ovolval3  40198  ovolval4lem2  40201  ovolval5lem2  40204  ovnovollem1  40207  ovnovollem2  40208  ovnovollem3  40209  vonvolmbllem  40211  vonvolmbl  40212  vitali2  40245  issmflem  40273  incsmf  40288  decsmf  40312  nsssmfmbflem  40323  smfresal  40332  smfmullem4  40338  smf2id  40345  refdivpm  41660  elbigo2  41668  elbigof  41670  elbigodm  41671  elbigoimp  41672  elbigolo1  41673  amgmlemALT  41882
  Copyright terms: Public domain W3C validator