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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 10298 . 2 ℂ ∈ V
2 ax-resscn 10274 . 2 ℝ ⊆ ℂ
31, 2ssexi 4998 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  Vcvv 3391  cc 10215  cr 10216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-cnex 10273  ax-resscn 10274
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783
This theorem is referenced by:  reelprrecn  10309  negfi  11252  xrex  12039  limsuple  14428  limsuplt  14429  limsupbnd1  14432  rlim  14445  rlimf  14451  rlimss  14452  ello12  14466  lo1f  14468  lo1dm  14469  elo12  14477  o1f  14479  o1dm  14480  o1of2  14562  o1rlimmul  14568  o1add2  14573  o1mul2  14574  o1sub2  14575  o1dif  14579  caucvgrlem  14622  fsumo1  14762  rpnnen  15172  cpnnen  15174  ruclem13  15187  ruc  15188  aleph1re  15190  aleph1irr  15191  cnfldds  19960  replusg  20161  remulr  20162  rele2  20165  reds  20167  refldcj  20171  ismet  22338  tngngp2  22666  tngngpd  22667  tngngp  22668  tngngp3  22670  nrmtngnrm  22672  tngnrg  22688  rerest  22817  xrtgioo  22819  xrrest  22820  xrsmopn  22825  opnreen  22844  rectbntr0  22845  xrge0tsms  22847  bcthlem1  23331  bcthlem5  23335  reust  23380  rrxip  23389  pmltpclem2  23429  ovolficcss  23449  ovolval  23453  elovolmlem  23454  ovolctb2  23472  ismbl  23506  mblsplit  23512  voliunlem3  23532  dyadmbl  23580  vitalilem2  23589  vitalilem3  23590  vitalilem4  23591  vitalilem5  23592  vitali  23593  mbff  23605  ismbf  23608  ismbfcn  23609  mbfconst  23613  cncombf  23638  cnmbf  23639  0plef  23652  i1fd  23661  itg1ge0  23666  i1faddlem  23673  i1fmullem  23674  i1fadd  23675  i1fmul  23676  itg1addlem4  23679  i1fmulclem  23682  i1fmulc  23683  itg1mulc  23684  i1fsub  23688  itg1sub  23689  itg1lea  23692  itg1le  23693  mbfi1fseqlem2  23696  mbfi1fseqlem4  23698  mbfi1fseqlem5  23699  mbfi1flimlem  23702  mbfmullem2  23704  itg2val  23708  xrge0f  23711  itg2ge0  23715  itg2itg1  23716  itg20  23717  itg2le  23719  itg2const  23720  itg2const2  23721  itg2seq  23722  itg2uba  23723  itg2lea  23724  itg2mulclem  23726  itg2mulc  23727  itg2splitlem  23728  itg2split  23729  itg2monolem1  23730  itg2mono  23733  itg2i1fseqle  23734  itg2i1fseq  23735  itg2addlem  23738  itg2gt0  23740  itg2cnlem1  23741  itg2cnlem2  23742  iblss  23784  i1fibl  23787  itgitg1  23788  itgle  23789  ibladdlem  23799  itgaddlem1  23802  iblabslem  23807  iblabs  23808  iblabsr  23809  iblmulc2  23810  itgmulc2lem1  23811  bddmulibl  23818  dvnfre  23928  c1liplem1  23972  c1lip2  23974  lhop2  23991  dvcnvrelem2  23994  taylthlem2  24341  dmarea  24897  vmadivsum  25384  rpvmasumlem  25389  mudivsum  25432  selberglem1  25447  selberglem2  25448  selberg2lem  25452  selberg2  25453  pntrsumo1  25467  selbergr  25470  iscgrgd  25621  elee  25987  xrge0tsmsd  30109  nn0omnd  30165  xrge0slmod  30168  raddcn  30299  rrhcn  30365  qqtopn  30379  dmvlsiga  30516  ddeval1  30621  ddeval0  30622  ddemeas  30623  mbfmcnt  30654  sxbrsigalem0  30657  sxbrsigalem3  30658  sxbrsigalem2  30672  isrrvv  30829  dstfrvclim1  30863  signsplypnf  30951  erdsze2lem1  31506  erdsze2lem2  31507  snmlval  31634  knoppcnlem5  32802  knoppcnlem6  32803  knoppcnlem7  32804  knoppcnlem8  32805  cnndvlem2  32844  icoreresf  33514  icoreval  33515  poimirlem29  33749  poimirlem30  33750  poimirlem31  33751  poimir  33753  broucube  33754  mblfinlem3  33759  itg2addnclem  33771  itg2addnclem3  33773  itg2addnc  33774  itg2gt0cn  33775  ibladdnclem  33776  itgaddnclem1  33778  iblabsnclem  33783  iblabsnc  33784  iblmulc2nc  33785  itgmulc2nclem1  33786  bddiblnc  33790  ftc1anclem3  33797  ftc1anclem4  33798  ftc1anclem5  33799  ftc1anclem6  33800  ftc1anclem7  33801  ftc1anclem8  33802  ftc1anc  33803  filbcmb  33845  rrncmslem  33940  repwsmet  33942  rrnequiv  33943  ismrer1  33946  pell1qrval  37909  pell14qrval  37911  pell1234qrval  37913  k0004ss1  38946  addrval  39165  subrval  39166  mulvval  39167  climreeq  40322  limsupre  40350  limcresiooub  40351  limcresioolb  40352  limsuppnfdlem  40410  limsuppnflem  40419  limsupmnflem  40429  limsupre2lem  40433  xlimclim  40527  icccncfext  40577  cncfiooicclem1  40583  itgsubsticclem  40667  ovolsplit  40681  dirkerval  40784  dirkercncflem4  40799  fourierdlem14  40814  fourierdlem15  40815  fourierdlem32  40832  fourierdlem33  40833  fourierdlem54  40853  fourierdlem62  40861  fourierdlem70  40869  fourierdlem81  40880  fourierdlem92  40891  fourierdlem102  40901  fourierdlem111  40910  fourierdlem114  40913  etransclem2  40929  rrxtopn0  40989  qndenserrnbllem  40990  qndenserrnbl  40991  qndenserrn  40995  rrnprjdstle  40997  ioorrnopnlem  41000  dmvolsal  41040  hoicvr  41241  hoissrrn  41242  hoiprodcl2  41248  hoicvrrex  41249  ovn0lem  41258  ovn02  41261  hsphoif  41269  hoidmvval  41270  hoissrrn2  41271  hsphoival  41272  hoidmvlelem3  41290  hoidmvle  41293  ovnhoilem1  41294  ovnhoilem2  41295  ovnhoi  41296  hspval  41302  ovnlecvr2  41303  ovncvr2  41304  hoidifhspval2  41308  hoiqssbl  41318  hspmbllem2  41320  hspmbl  41322  hoimbl  41324  opnvonmbllem2  41326  ovolval2lem  41336  ovolval2  41337  ovolval3  41340  ovolval4lem2  41343  ovolval5lem2  41346  ovnovollem1  41349  ovnovollem2  41350  ovnovollem3  41351  vonvolmbllem  41353  vonvolmbl  41354  vitali2  41387  issmflem  41415  incsmf  41430  decsmf  41454  nsssmfmbflem  41465  smfresal  41474  smfmullem4  41480  smf2id  41487  refdivpm  42903  elbigo2  42911  elbigof  42913  elbigodm  42914  elbigoimp  42915  elbigolo1  42916  amgmlemALT  43117
  Copyright terms: Public domain W3C validator