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

Theorem rexr 11202
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
rexr (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr
StepHypRef Expression
1 ressxr 11200 . 2 ℝ ⊆ ℝ*
21sseli 3941 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  *cxr 11189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-un 3916  df-in 3918  df-ss 3928  df-xr 11194
This theorem is referenced by:  rexri  11214  lenlt  11234  ltpnf  13042  mnflt  13045  xrltnsym  13057  xrlttr  13060  xrre  13089  xrre3  13091  max1  13105  max2  13107  min1  13109  min2  13110  maxle  13111  lemin  13112  maxlt  13113  ltmin  13114  max0sub  13116  qbtwnxr  13120  xralrple  13125  alrple  13126  xltnegi  13136  rexadd  13152  xaddnemnf  13156  xaddnepnf  13157  xaddcom  13160  xnegdi  13168  xpncan  13171  xnpcan  13172  xleadd1a  13173  xleadd1  13175  xltadd1  13176  xltadd2  13177  xsubge0  13181  rexmul  13191  xadddilem  13214  xadddir  13216  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxrun  13236  supxrunb1  13239  supxrunb2  13240  supxrbnd1  13241  supxrbnd2  13242  xrsup0  13243  supxrbnd  13248  infmremnf  13263  elioo4g  13325  elioc2  13328  elico2  13329  elicc2  13330  iccss  13333  iooshf  13344  iooneg  13389  icoshft  13391  difreicc  13402  hashbnd  14237  elicc4abs  15205  icodiamlt  15321  limsupgord  15355  pcadd  16762  ramubcl  16891  lt6abl  19673  xrsmcmn  20823  xrs1mnd  20838  xrs10  20839  xrsdsreval  20845  psmetge0  23668  xmetge0  23700  imasdsf1olem  23729  bl2in  23756  blssps  23780  blss  23781  blcld  23864  icopnfcld  24134  iocmnfcld  24135  bl2ioo  24158  blssioo  24161  xrtgioo  24172  xrsblre  24177  iccntr  24187  icccmplem2  24189  icccmp  24191  reconnlem2  24193  xrge0tsms  24200  icoopnst  24305  iocopnst  24306  ovolfioo  24834  ovolicc2lem1  24884  ovolicc2lem5  24888  voliunlem3  24919  icombl1  24930  icombl  24931  iccvolcl  24934  ovolioo  24935  ioovolcl  24937  uniiccdif  24945  volsup2  24972  mbfimasn  24999  ismbf3d  25021  mbfsup  25031  itg2seq  25110  bddiblnc  25209  dvlip2  25362  ply1remlem  25530  abelthlem3  25795  abelth  25803  sincosq2sgn  25859  sincosq3sgn  25860  sinq12ge0  25868  sincos6thpi  25875  sineq0  25883  efif1olem1  25901  efif1olem2  25902  efif1o  25905  eff1o  25908  loglesqrt  26114  basellem1  26433  pntlemo  26958  nmobndi  29720  nmopub2tALT  30854  nmfnleub2  30871  nmopcoadji  31046  rexdiv  31785  xrge0tsmsd  31902  pnfneige0  32535  lmxrge0  32536  hashf2  32686  sxbrsigalem0  32874  orvcgteel  33070  orvclteel  33075  sgnclre  33142  sgnneg  33143  signstfvn  33184  signstfvneq0  33187  signsvfn  33197  ivthALT  34810  icorempo  35825  icoreunrn  35833  iooelexlt  35836  relowlssretop  35837  relowlpssretop  35838  poimir  36114  mblfinlem2  36119  iblabsnclem  36144  ftc1anclem1  36154  ftc1anclem6  36159  areacirclem5  36173  areacirc  36174  blbnd  36249  iocmbl  41550  reabssgn  41915  supxrre3  43566  supxrgere  43574  infrpge  43592  infxrunb2  43609  infxrbnd2  43610  infleinflem2  43612  xrralrecnnle  43624  supxrunb3  43641  supminfxr2  43711  xrpnf  43728  ioomidp  43759  limsupre  43889  limsupub  43952  limsuppnflem  43958  limsupre3lem  43980  liminfgord  44002  liminflelimsuplem  44023  limsupgtlem  44025  limsupub2  44060  xlimpnfxnegmnf  44062  xlimmnfvlem2  44081  xlimmnfv  44082  xlimpnfvlem2  44085  xlimpnfv  44086  icccncfext  44135  volioc  44220  volico  44231  fourierdlem113  44467  meaiuninclem  44728  meaiuninc3v  44732  icoresmbl  44791  ovolval5lem1  44900  mbfresmf  44987  cnfsmf  44988  incsmf  44990  smfconst  44997  decsmf  45015  smfres  45038  smfco  45050  issmfle2d  45057  finfdm  45094  bgoldbtbndlem3  46006  rrxsphere  46841  i0oii  46959  io1ii  46960
  Copyright terms: Public domain W3C validator