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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 10055 . 2 ℂ ∈ V
2 ax-resscn 10031 . 2 ℝ ⊆ ℂ
31, 2ssexi 4836 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cc 9972  cr 9973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-cnex 10030  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621
This theorem is referenced by:  reelprrecn  10066  negfi  11009  xrex  11867  limsuple  14253  limsuplt  14254  limsupbnd1  14257  rlim  14270  rlimf  14276  rlimss  14277  ello12  14291  lo1f  14293  lo1dm  14294  elo12  14302  o1f  14304  o1dm  14305  o1of2  14387  o1rlimmul  14393  o1add2  14398  o1mul2  14399  o1sub2  14400  o1dif  14404  caucvgrlem  14447  fsumo1  14588  rpnnen  15000  cpnnen  15002  ruclem13  15015  ruc  15016  aleph1re  15018  aleph1irr  15019  cnfldds  19804  replusg  20004  remulr  20005  rele2  20008  reds  20010  refldcj  20014  ismet  22175  tngngp2  22503  tngngpd  22504  tngngp  22505  tngngp3  22507  nrmtngnrm  22509  tngnrg  22525  rerest  22654  xrtgioo  22656  xrrest  22657  xrsmopn  22662  opnreen  22681  rectbntr0  22682  xrge0tsms  22684  bcthlem1  23167  bcthlem5  23171  reust  23215  rrxip  23224  pmltpclem2  23264  ovolficcss  23284  ovolval  23288  elovolm  23289  elovolmr  23290  ovolmge0  23291  ovolgelb  23294  ovolctb2  23306  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovolshftlem2  23324  ovolicc2  23336  ismbl  23340  mblsplit  23346  voliunlem3  23366  ioombl1  23376  dyadmbl  23414  vitalilem2  23423  vitalilem3  23424  vitalilem4  23425  vitalilem5  23426  vitali  23427  mbff  23439  ismbf  23442  ismbfcn  23443  mbfconst  23447  cncombf  23470  cnmbf  23471  0plef  23484  i1fd  23493  itg1ge0  23498  i1faddlem  23505  i1fmullem  23506  i1fadd  23507  i1fmul  23508  itg1addlem4  23511  i1fmulclem  23514  i1fmulc  23515  itg1mulc  23516  i1fsub  23520  itg1sub  23521  itg1lea  23524  itg1le  23525  mbfi1fseqlem2  23528  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1flimlem  23534  mbfmullem2  23536  itg2val  23540  xrge0f  23543  itg2ge0  23547  itg2itg1  23548  itg20  23549  itg2le  23551  itg2const  23552  itg2const2  23553  itg2seq  23554  itg2uba  23555  itg2lea  23556  itg2mulclem  23558  itg2mulc  23559  itg2splitlem  23560  itg2split  23561  itg2monolem1  23562  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq  23567  itg2addlem  23570  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  iblss  23616  i1fibl  23619  itgitg1  23620  itgle  23621  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgmulc2lem1  23643  bddmulibl  23650  dvnfre  23760  c1liplem1  23804  c1lip2  23806  lhop2  23823  dvcnvrelem2  23826  taylthlem2  24173  dmarea  24729  vmadivsum  25216  rpvmasumlem  25221  mudivsum  25264  selberglem1  25279  selberglem2  25280  selberg2lem  25284  selberg2  25285  pntrsumo1  25299  selbergr  25302  iscgrgd  25453  elee  25819  xrge0tsmsd  29913  nn0omnd  29969  xrge0slmod  29972  raddcn  30103  rrhcn  30169  qqtopn  30183  dmvlsiga  30320  ddeval1  30425  ddeval0  30426  ddemeas  30427  mbfmcnt  30458  sxbrsigalem0  30461  sxbrsigalem3  30462  sxbrsigalem2  30476  isrrvv  30633  dstfrvclim1  30667  signsplypnf  30755  erdsze2lem1  31311  erdsze2lem2  31312  snmlval  31439  knoppcnlem5  32612  knoppcnlem6  32613  knoppcnlem7  32614  knoppcnlem8  32615  cnndvlem2  32654  icoreresf  33330  icoreval  33331  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimir  33572  broucube  33573  mblfinlem3  33578  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nclem1  33606  bddiblnc  33610  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  filbcmb  33665  rrncmslem  33761  repwsmet  33763  rrnequiv  33764  ismrer1  33767  pell1qrval  37727  pell14qrval  37729  pell1234qrval  37731  k0004ss1  38766  addrval  38987  subrval  38988  mulvval  38989  climreeq  40163  limsupre  40191  limcresiooub  40192  limcresioolb  40193  limsuppnfdlem  40251  limsuppnflem  40260  limsupmnflem  40270  limsupre2lem  40274  xlimclim  40368  icccncfext  40418  cncfiooicclem1  40424  itgsubsticclem  40509  ovolsplit  40523  dirkerval  40626  dirkercncflem4  40641  fourierdlem14  40656  fourierdlem15  40657  fourierdlem32  40674  fourierdlem33  40675  fourierdlem54  40695  fourierdlem62  40703  fourierdlem70  40711  fourierdlem81  40722  fourierdlem92  40733  fourierdlem102  40743  fourierdlem111  40752  fourierdlem114  40755  etransclem2  40771  rrxtopn0  40831  qndenserrnbllem  40832  qndenserrnbl  40833  qndenserrn  40837  rrnprjdstle  40839  ioorrnopnlem  40842  dmvolsal  40882  hoicvr  41083  hoissrrn  41084  hoiprodcl2  41090  hoicvrrex  41091  ovn0lem  41100  ovn02  41103  hsphoif  41111  hoidmvval  41112  hoissrrn2  41113  hsphoival  41114  hoidmvlelem3  41132  hoidmvle  41135  ovnhoilem1  41136  ovnhoilem2  41137  ovnhoi  41138  hspval  41144  ovnlecvr2  41145  ovncvr2  41146  hoidifhspval2  41150  hoiqssbl  41160  hspmbllem2  41162  hspmbl  41164  hoimbl  41166  opnvonmbllem2  41168  ovolval2lem  41178  ovolval2  41179  ovolval3  41182  ovolval4lem2  41185  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  ovnovollem3  41193  vonvolmbllem  41195  vonvolmbl  41196  vitali2  41229  issmflem  41257  incsmf  41272  decsmf  41296  nsssmfmbflem  41307  smfresal  41316  smfmullem4  41322  smf2id  41329  refdivpm  42663  elbigo2  42671  elbigof  42673  elbigodm  42674  elbigoimp  42675  elbigolo1  42676  amgmlemALT  42877
  Copyright terms: Public domain W3C validator