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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 10603 . 2 ℂ ∈ V
2 ax-resscn 10579 . 2 ℝ ⊆ ℂ
31, 2ssexi 5207 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  Vcvv 3479  cc 10520  cr 10521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-sep 5184  ax-cnex 10578  ax-resscn 10579
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3141  df-v 3481  df-in 3925  df-ss 3935
This theorem is referenced by:  reelprrecn  10614  negfi  11574  xrex  12372  limsuple  14824  limsuplt  14825  limsupbnd1  14828  rlim  14841  rlimf  14847  rlimss  14848  ello12  14862  lo1f  14864  lo1dm  14865  elo12  14873  o1f  14875  o1dm  14876  o1of2  14958  o1rlimmul  14964  o1add2  14969  o1mul2  14970  o1sub2  14971  o1dif  14975  caucvgrlem  15018  fsumo1  15156  rpnnen  15569  cpnnen  15571  ruclem13  15584  ruc  15585  aleph1re  15587  aleph1irr  15588  cnfldds  20541  replusg  20740  remulr  20741  rele2  20744  reds  20746  refldcj  20750  ismet  22919  tngngp2  23247  tngngpd  23248  tngngp  23249  tngngp3  23251  nrmtngnrm  23253  tngnrg  23269  rerest  23398  xrtgioo  23400  xrrest  23401  xrsmopn  23406  opnreen  23425  rectbntr0  23426  xrge0tsms  23428  bcthlem1  23917  bcthlem5  23921  reust  23974  rrxip  23983  rrx0el  23991  ehl0base  24009  ehl1eudis  24013  ehl2eudis  24015  pmltpclem2  24042  ovolficcss  24062  ovolval  24066  elovolmlem  24067  ovolctb2  24085  ismbl  24119  mblsplit  24125  voliunlem3  24145  dyadmbl  24193  vitalilem2  24202  vitalilem3  24203  vitalilem4  24204  vitalilem5  24205  vitali  24206  mbff  24218  ismbf  24221  ismbfcn  24222  mbfconst  24226  cncombf  24251  cnmbf  24252  0plef  24265  i1fd  24274  itg1ge0  24279  i1faddlem  24286  i1fmullem  24287  i1fadd  24288  i1fmul  24289  itg1addlem4  24292  i1fmulclem  24295  i1fmulc  24296  itg1mulc  24297  i1fsub  24301  itg1sub  24302  itg1lea  24305  itg1le  24306  mbfi1fseqlem2  24309  mbfi1fseqlem4  24311  mbfi1fseqlem5  24312  mbfi1flimlem  24315  mbfmullem2  24317  itg2val  24321  xrge0f  24324  itg2ge0  24328  itg2itg1  24329  itg20  24330  itg2le  24332  itg2const  24333  itg2const2  24334  itg2seq  24335  itg2uba  24336  itg2lea  24337  itg2mulclem  24339  itg2mulc  24340  itg2splitlem  24341  itg2split  24342  itg2monolem1  24343  itg2mono  24346  itg2i1fseqle  24347  itg2i1fseq  24348  itg2addlem  24351  itg2gt0  24353  itg2cnlem1  24354  itg2cnlem2  24355  iblss  24397  i1fibl  24400  itgitg1  24401  itgle  24402  ibladdlem  24412  itgaddlem1  24415  iblabslem  24420  iblabs  24421  iblabsr  24422  iblmulc2  24423  itgmulc2lem1  24424  bddmulibl  24431  bddiblnc  24434  dvnfre  24544  c1liplem1  24588  c1lip2  24590  lhop2  24607  dvcnvrelem2  24610  taylthlem2  24958  dmarea  25532  vmadivsum  26055  rpvmasumlem  26060  mudivsum  26103  selberglem1  26118  selberglem2  26119  selberg2lem  26123  selberg2  26124  pntrsumo1  26138  selbergr  26141  iscgrgd  26296  elee  26677  xrge0tsmsd  30710  nn0omnd  30932  xrge0slmod  30935  raddcn  31190  rrhcn  31256  qqtopn  31270  dmvlsiga  31406  ddeval1  31511  ddeval0  31512  ddemeas  31513  mbfmcnt  31544  sxbrsigalem0  31547  sxbrsigalem3  31548  sxbrsigalem2  31562  isrrvv  31719  dstfrvclim1  31753  signsplypnf  31838  erdsze2lem1  32468  erdsze2lem2  32469  snmlval  32596  knoppcnlem5  33854  knoppcnlem6  33855  knoppcnlem7  33856  knoppcnlem8  33857  cnndvlem2  33895  icoreresf  34671  icoreval  34672  poimirlem29  34986  poimirlem30  34987  poimirlem31  34988  poimir  34990  broucube  34991  mblfinlem3  34996  itg2addnclem  35008  itg2addnclem3  35010  itg2addnc  35011  itg2gt0cn  35012  ibladdnclem  35013  itgaddnclem1  35015  iblabsnclem  35020  iblabsnc  35021  iblmulc2nc  35022  itgmulc2nclem1  35023  ftc1anclem3  35032  ftc1anclem4  35033  ftc1anclem5  35034  ftc1anclem6  35035  ftc1anclem7  35036  ftc1anclem8  35037  ftc1anc  35038  filbcmb  35078  rrncmslem  35170  repwsmet  35172  rrnequiv  35173  ismrer1  35176  pell1qrval  39619  pell14qrval  39621  pell1234qrval  39623  k0004ss1  40689  addrval  41006  subrval  41007  mulvval  41008  climreeq  42097  limsupre  42125  limcresiooub  42126  limcresioolb  42127  limsuppnfdlem  42185  limsuppnflem  42194  limsupmnflem  42204  limsupre2lem  42208  xlimclim  42308  icccncfext  42371  cncfiooicclem1  42377  itgsubsticclem  42459  ovolsplit  42472  dirkerval  42575  dirkercncflem4  42590  fourierdlem14  42605  fourierdlem15  42606  fourierdlem32  42623  fourierdlem33  42624  fourierdlem54  42644  fourierdlem62  42652  fourierdlem70  42660  fourierdlem81  42671  fourierdlem92  42682  fourierdlem102  42692  fourierdlem111  42701  fourierdlem114  42704  etransclem2  42720  rrxtopn0  42777  qndenserrnbllem  42778  qndenserrnbl  42779  qndenserrn  42783  rrnprjdstle  42785  ioorrnopnlem  42788  dmvolsal  42828  hoicvr  43029  hoissrrn  43030  hoiprodcl2  43036  hoicvrrex  43037  ovn0lem  43046  ovn02  43049  hsphoif  43057  hoidmvval  43058  hoissrrn2  43059  hsphoival  43060  hoidmvlelem3  43078  hoidmvle  43081  ovnhoilem1  43082  ovnhoilem2  43083  ovnhoi  43084  hspval  43090  ovnlecvr2  43091  ovncvr2  43092  hoidifhspval2  43096  hoiqssbl  43106  hspmbllem2  43108  hspmbl  43110  hoimbl  43112  opnvonmbllem2  43114  ovolval2lem  43124  ovolval2  43125  ovolval3  43128  ovolval4lem2  43131  ovolval5lem2  43134  ovnovollem1  43137  ovnovollem2  43138  ovnovollem3  43139  vonvolmbllem  43141  vonvolmbl  43142  vitali2  43175  issmflem  43203  incsmf  43218  decsmf  43242  nsssmfmbflem  43253  smfresal  43262  smfmullem4  43268  smf2id  43275  refdivpm  44799  elbigo2  44807  elbigof  44809  elbigodm  44810  elbigoimp  44811  elbigolo1  44812  prelrrx2  44957  rrx2xpref1o  44962  rrx2xpreen  44963  rrx2linesl  44987  line2  44996  line2x  44998  line2y  44999  amgmlemALT  45161
  Copyright terms: Public domain W3C validator