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

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

Proof of Theorem reex
StepHypRef Expression
1 cnex 9870 . 2 ℂ ∈ V
2 ax-resscn 9846 . 2 ℝ ⊆ ℂ
31, 2ssexi 4723 1 ℝ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3169  cc 9787  cr 9788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-cnex 9845  ax-resscn 9846
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550
This theorem is referenced by:  reelprrecn  9881  negfi  10817  xrex  11658  limsuple  14000  limsuplt  14001  limsupbnd1  14004  rlim  14017  rlimf  14023  rlimss  14024  ello12  14038  lo1f  14040  lo1dm  14041  elo12  14049  o1f  14051  o1dm  14052  o1of2  14134  o1rlimmul  14140  o1add2  14145  o1mul2  14146  o1sub2  14147  o1dif  14151  caucvgrlem  14194  fsumo1  14328  rpnnen  14738  cpnnen  14740  ruclem13  14753  ruc  14754  aleph1re  14756  aleph1irr  14757  cnfldds  19520  replusg  19717  remulr  19718  rele2  19721  reds  19723  refldcj  19727  ismet  21876  tngngp2  22201  tngngpd  22202  tngngp  22203  tngnrg  22218  rerest  22344  xrtgioo  22346  xrrest  22347  xrsmopn  22352  opnreen  22371  rectbntr0  22372  xrge0tsms  22374  bcthlem1  22843  bcthlem5  22847  reust  22891  rrxip  22900  pmltpclem2  22939  ovolficcss  22959  ovolval  22963  elovolm  22964  elovolmr  22965  ovolmge0  22966  ovolgelb  22969  ovolctb2  22981  ovolunlem1a  22985  ovolunlem1  22986  ovoliunlem1  22991  ovoliunlem2  22992  ovolshftlem2  22999  ovolicc2  23011  ismbl  23015  mblsplit  23021  voliunlem3  23041  ioombl1  23051  dyadmbl  23088  vitalilem2  23098  vitalilem3  23099  vitalilem4  23100  vitalilem5  23101  vitali  23102  mbff  23114  ismbf  23117  ismbfcn  23118  mbfconst  23122  cncombf  23145  cnmbf  23146  0plef  23159  i1fd  23168  itg1ge0  23173  i1faddlem  23180  i1fmullem  23181  i1fadd  23182  i1fmul  23183  itg1addlem4  23186  i1fmulclem  23189  i1fmulc  23190  itg1mulc  23191  i1fsub  23195  itg1sub  23196  itg1lea  23199  itg1le  23200  mbfi1fseqlem2  23203  mbfi1fseqlem4  23205  mbfi1fseqlem5  23206  mbfi1flimlem  23209  mbfmullem2  23211  itg2val  23215  xrge0f  23218  itg2ge0  23222  itg2itg1  23223  itg20  23224  itg2le  23226  itg2const  23227  itg2const2  23228  itg2seq  23229  itg2uba  23230  itg2lea  23231  itg2mulclem  23233  itg2mulc  23234  itg2splitlem  23235  itg2split  23236  itg2monolem1  23237  itg2mono  23240  itg2i1fseqle  23241  itg2i1fseq  23242  itg2addlem  23245  itg2gt0  23247  itg2cnlem1  23248  itg2cnlem2  23249  iblss  23291  i1fibl  23294  itgitg1  23295  itgle  23296  ibladdlem  23306  itgaddlem1  23309  iblabslem  23314  iblabs  23315  iblabsr  23316  iblmulc2  23317  itgmulc2lem1  23318  bddmulibl  23325  dvnfre  23435  c1liplem1  23477  c1lip2  23479  lhop2  23496  dvcnvrelem2  23499  taylthlem2  23846  dmarea  24398  vmadivsum  24885  rpvmasumlem  24890  mudivsum  24933  selberglem1  24948  selberglem2  24949  selberg2lem  24953  selberg2  24954  pntrsumo1  24968  selbergr  24971  iscgrgd  25123  elee  25489  xrge0tsmsd  28919  nn0omnd  28975  xrge0slmod  28978  raddcn  29106  rrhcn  29172  qqtopn  29186  dmvlsiga  29322  ddeval1  29427  ddeval0  29428  ddemeas  29429  mbfmcnt  29460  sxbrsigalem0  29463  sxbrsigalem3  29464  sxbrsigalem2  29478  isrrvv  29635  dstfrvclim1  29669  signsplypnf  29756  erdsze2lem1  30242  erdsze2lem2  30243  snmlval  30370  knoppcnlem5  31460  knoppcnlem6  31461  knoppcnlem7  31462  knoppcnlem8  31463  cnndvlem2  31502  icoreresf  32176  icoreval  32177  poimirlem29  32408  poimirlem30  32409  poimirlem31  32410  poimir  32412  broucube  32413  mblfinlem3  32418  itg2addnclem  32431  itg2addnclem3  32433  itg2addnc  32434  itg2gt0cn  32435  ibladdnclem  32436  itgaddnclem1  32438  iblabsnclem  32443  iblabsnc  32444  iblmulc2nc  32445  itgmulc2nclem1  32446  bddiblnc  32450  ftc1anclem3  32457  ftc1anclem4  32458  ftc1anclem5  32459  ftc1anclem6  32460  ftc1anclem7  32461  ftc1anclem8  32462  ftc1anc  32463  filbcmb  32505  rrncmslem  32601  repwsmet  32603  rrnequiv  32604  ismrer1  32607  pell1qrval  36228  pell14qrval  36230  pell1234qrval  36232  k0004ss1  37269  addrval  37491  subrval  37492  mulvval  37493  climreeq  38481  limsupre  38509  limcresiooub  38510  limcresioolb  38511  icccncfext  38574  cncfiooicclem1  38580  itgsubsticclem  38668  ovolsplit  38682  dirkerval  38785  dirkercncflem4  38800  fourierdlem14  38815  fourierdlem15  38816  fourierdlem32  38833  fourierdlem33  38834  fourierdlem54  38854  fourierdlem62  38862  fourierdlem70  38870  fourierdlem81  38881  fourierdlem92  38892  fourierdlem102  38902  fourierdlem111  38911  fourierdlem114  38914  etransclem2  38930  rrxtopn0  38990  qndenserrnbllem  38991  qndenserrnbl  38992  qndenserrn  38996  rrnprjdstle  38998  ioorrnopnlem  39001  dmvolsal  39041  hoicvr  39239  hoissrrn  39240  hoiprodcl2  39246  hoicvrrex  39247  ovn0lem  39256  ovn02  39259  hsphoif  39267  hoidmvval  39268  hoissrrn2  39269  hsphoival  39270  hoidmvlelem3  39288  hoidmvle  39291  ovnhoilem1  39292  ovnhoilem2  39293  ovnhoi  39294  hspval  39300  ovnlecvr2  39301  ovncvr2  39302  hoidifhspval2  39306  hoiqssbl  39316  hspmbllem2  39318  hspmbl  39320  hoimbl  39322  opnvonmbllem2  39324  ovolval2lem  39334  ovolval2  39335  ovolval3  39338  ovolval4lem2  39341  ovolval5lem2  39344  ovnovollem1  39347  ovnovollem2  39348  ovnovollem3  39349  vonvolmbllem  39351  vonvolmbl  39352  vitali2  39386  issmflem  39414  incsmf  39430  decsmf  39454  nsssmfmbflem  39465  smfresal  39474  smfmullem4  39480  smf2id  39487  refdivpm  42135  elbigo2  42143  elbigof  42145  elbigodm  42146  elbigoimp  42147  elbigolo1  42148  amgmlemALT  42318
  Copyright terms: Public domain W3C validator