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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 10607 . 2 ℂ ∈ V
2 ax-resscn 10583 . 2 ℝ ⊆ ℂ
31, 2ssexi 5218 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495  cc 10524  cr 10525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-in 3942  df-ss 3951
This theorem is referenced by:  reelprrecn  10618  negfi  11578  xrex  12376  limsuple  14825  limsuplt  14826  limsupbnd1  14829  rlim  14842  rlimf  14848  rlimss  14849  ello12  14863  lo1f  14865  lo1dm  14866  elo12  14874  o1f  14876  o1dm  14877  o1of2  14959  o1rlimmul  14965  o1add2  14970  o1mul2  14971  o1sub2  14972  o1dif  14976  caucvgrlem  15019  fsumo1  15157  rpnnen  15570  cpnnen  15572  ruclem13  15585  ruc  15586  aleph1re  15588  aleph1irr  15589  cnfldds  20485  replusg  20684  remulr  20685  rele2  20688  reds  20690  refldcj  20694  ismet  22862  tngngp2  23190  tngngpd  23191  tngngp  23192  tngngp3  23194  nrmtngnrm  23196  tngnrg  23212  rerest  23341  xrtgioo  23343  xrrest  23344  xrsmopn  23349  opnreen  23368  rectbntr0  23369  xrge0tsms  23371  bcthlem1  23856  bcthlem5  23860  reust  23913  rrxip  23922  rrx0el  23930  ehl0base  23948  ehl1eudis  23952  ehl2eudis  23954  pmltpclem2  23979  ovolficcss  23999  ovolval  24003  elovolmlem  24004  ovolctb2  24022  ismbl  24056  mblsplit  24062  voliunlem3  24082  dyadmbl  24130  vitalilem2  24139  vitalilem3  24140  vitalilem4  24141  vitalilem5  24142  vitali  24143  mbff  24155  ismbf  24158  ismbfcn  24159  mbfconst  24163  cncombf  24188  cnmbf  24189  0plef  24202  i1fd  24211  itg1ge0  24216  i1faddlem  24223  i1fmullem  24224  i1fadd  24225  i1fmul  24226  itg1addlem4  24229  i1fmulclem  24232  i1fmulc  24233  itg1mulc  24234  i1fsub  24238  itg1sub  24239  itg1lea  24242  itg1le  24243  mbfi1fseqlem2  24246  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1flimlem  24252  mbfmullem2  24254  itg2val  24258  xrge0f  24261  itg2ge0  24265  itg2itg1  24266  itg20  24267  itg2le  24269  itg2const  24270  itg2const2  24271  itg2seq  24272  itg2uba  24273  itg2lea  24274  itg2mulclem  24276  itg2mulc  24277  itg2splitlem  24278  itg2split  24279  itg2monolem1  24280  itg2mono  24283  itg2i1fseqle  24284  itg2i1fseq  24285  itg2addlem  24288  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  iblss  24334  i1fibl  24337  itgitg1  24338  itgle  24339  ibladdlem  24349  itgaddlem1  24352  iblabslem  24357  iblabs  24358  iblabsr  24359  iblmulc2  24360  itgmulc2lem1  24361  bddmulibl  24368  dvnfre  24478  c1liplem1  24522  c1lip2  24524  lhop2  24541  dvcnvrelem2  24544  taylthlem2  24891  dmarea  25463  vmadivsum  25986  rpvmasumlem  25991  mudivsum  26034  selberglem1  26049  selberglem2  26050  selberg2lem  26054  selberg2  26055  pntrsumo1  26069  selbergr  26072  iscgrgd  26227  elee  26608  xrge0tsmsd  30620  nn0omnd  30842  xrge0slmod  30845  raddcn  31072  rrhcn  31138  qqtopn  31152  dmvlsiga  31288  ddeval1  31393  ddeval0  31394  ddemeas  31395  mbfmcnt  31426  sxbrsigalem0  31429  sxbrsigalem3  31430  sxbrsigalem2  31444  isrrvv  31601  dstfrvclim1  31635  signsplypnf  31720  erdsze2lem1  32348  erdsze2lem2  32349  snmlval  32476  knoppcnlem5  33734  knoppcnlem6  33735  knoppcnlem7  33736  knoppcnlem8  33737  cnndvlem2  33775  icoreresf  34516  icoreval  34517  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimir  34807  broucube  34808  mblfinlem3  34813  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  itg2gt0cn  34829  ibladdnclem  34830  itgaddnclem1  34832  iblabsnclem  34837  iblabsnc  34838  iblmulc2nc  34839  itgmulc2nclem1  34840  bddiblnc  34844  ftc1anclem3  34851  ftc1anclem4  34852  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anclem8  34856  ftc1anc  34857  filbcmb  34898  rrncmslem  34993  repwsmet  34995  rrnequiv  34996  ismrer1  34999  pell1qrval  39323  pell14qrval  39325  pell1234qrval  39327  k0004ss1  40381  addrval  40678  subrval  40679  mulvval  40680  climreeq  41774  limsupre  41802  limcresiooub  41803  limcresioolb  41804  limsuppnfdlem  41862  limsuppnflem  41871  limsupmnflem  41881  limsupre2lem  41885  xlimclim  41985  icccncfext  42050  cncfiooicclem1  42056  itgsubsticclem  42140  ovolsplit  42154  dirkerval  42257  dirkercncflem4  42272  fourierdlem14  42287  fourierdlem15  42288  fourierdlem32  42305  fourierdlem33  42306  fourierdlem54  42326  fourierdlem62  42334  fourierdlem70  42342  fourierdlem81  42353  fourierdlem92  42364  fourierdlem102  42374  fourierdlem111  42383  fourierdlem114  42386  etransclem2  42402  rrxtopn0  42459  qndenserrnbllem  42460  qndenserrnbl  42461  qndenserrn  42465  rrnprjdstle  42467  ioorrnopnlem  42470  dmvolsal  42510  hoicvr  42711  hoissrrn  42712  hoiprodcl2  42718  hoicvrrex  42719  ovn0lem  42728  ovn02  42731  hsphoif  42739  hoidmvval  42740  hoissrrn2  42741  hsphoival  42742  hoidmvlelem3  42760  hoidmvle  42763  ovnhoilem1  42764  ovnhoilem2  42765  ovnhoi  42766  hspval  42772  ovnlecvr2  42773  ovncvr2  42774  hoidifhspval2  42778  hoiqssbl  42788  hspmbllem2  42790  hspmbl  42792  hoimbl  42794  opnvonmbllem2  42796  ovolval2lem  42806  ovolval2  42807  ovolval3  42810  ovolval4lem2  42813  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  ovnovollem3  42821  vonvolmbllem  42823  vonvolmbl  42824  vitali2  42857  issmflem  42885  incsmf  42900  decsmf  42924  nsssmfmbflem  42935  smfresal  42944  smfmullem4  42950  smf2id  42957  refdivpm  44502  elbigo2  44510  elbigof  44512  elbigodm  44513  elbigoimp  44514  elbigolo1  44515  prelrrx2  44598  rrx2xpref1o  44603  rrx2xpreen  44604  rrx2linesl  44628  line2  44637  line2x  44639  line2y  44640  amgmlemALT  44802
  Copyright terms: Public domain W3C validator