Theorem rexr 11190

Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
rexr	⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr

Step	Hyp	Ref	Expression
1		ressxr 11188	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3931	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℝ^*cxr 11177

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-xr 11182

This theorem is referenced by:  rexri  11202  lenlt  11223  ltpnf  13046  mnflt  13049  xrltnsym  13063  xrlttr  13066  xrre  13096  xrre3  13098  max1  13112  max2  13114  min1  13116  min2  13117  maxle  13118  lemin  13119  maxlt  13120  ltmin  13121  max0sub  13123  qbtwnxr  13127  xralrple  13132  alrple  13133  xltnegi  13143  rexadd  13159  xaddnemnf  13163  xaddnepnf  13164  xaddcom  13167  xnegdi  13175  xpncan  13178  xnpcan  13179  xleadd1a  13180  xleadd1  13182  xltadd1  13183  xltadd2  13184  xsubge0  13188  rexmul  13198  xadddilem  13221  xadddir  13223  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxrun  13243  supxrunb1  13246  supxrunb2  13247  supxrbnd1  13248  supxrbnd2  13249  xrsup0  13250  supxrbnd  13255  infmremnf  13271  elioo4g  13334  elioc2  13337  elico2  13338  elicc2  13339  iccss  13342  iooshf  13354  iooneg  13399  icoshft  13401  difreicc  13412  hashbnd  14271  elicc4abs  15255  icodiamlt  15373  limsupgord  15407  pcadd  16829  ramubcl  16958  lt6abl  19836  xrsmcmn  21358  xrsdsreval  21378  xrs1mnd  21407  xrs10  21408  psmetge0  24268  xmetge0  24300  imasdsf1olem  24329  bl2in  24356  blssps  24380  blss  24381  blcld  24461  icopnfcld  24723  iocmnfcld  24724  bl2ioo  24748  blssioo  24751  xrtgioo  24763  xrsblre  24768  iccntr  24778  icccmplem2  24780  icccmp  24782  reconnlem2  24784  xrge0tsms  24791  icoopnst  24904  iocopnst  24905  ovolfioo  25436  ovolicc2lem1  25486  ovolicc2lem5  25490  voliunlem3  25521  icombl1  25532  icombl  25533  iccvolcl  25536  ovolioo  25537  ioovolcl  25539  uniiccdif  25547  volsup2  25574  mbfimasn  25601  ismbf3d  25623  mbfsup  25633  itg2seq  25711  bddiblnc  25811  dvlip2  25968  ply1remlem  26138  abelthlem3  26411  abelth  26419  sincosq2sgn  26476  sincosq3sgn  26477  sinq12ge0  26485  sincos6thpi  26493  sineq0  26501  efif1olem1  26519  efif1olem2  26520  efif1o  26523  eff1o  26526  loglesqrt  26739  basellem1  27059  pntlemo  27586  nmobndi  30862  nmopub2tALT  31996  nmfnleub2  32013  nmopcoadji  32188  sgnclre  32923  sgnneg  32924  rexdiv  33017  xrge0tsmsd  33166  pnfneige0  34128  lmxrge0  34129  hashf2  34261  sxbrsigalem0  34448  orvcgteel  34645  orvclteel  34650  signstfvn  34746  signstfvneq0  34749  signsvfn  34759  ivthALT  36548  icorempo  37600  icoreunrn  37608  iooelexlt  37611  relowlssretop  37612  relowlpssretop  37613  poimir  37898  mblfinlem2  37903  iblabsnclem  37928  ftc1anclem1  37938  ftc1anclem6  37943  areacirclem5  37957  areacirc  37958  blbnd  38032  iocmbl  43564  reabssgn  43986  supxrre3  45678  supxrgere  45686  infrpge  45704  infxrunb2  45720  infxrbnd2  45721  infleinflem2  45723  xrralrecnnle  45735  supxrunb3  45751  supminfxr2  45821  xrpnf  45837  ioomidp  45868  limsupre  45993  limsupub  46056  limsuppnflem  46062  limsupre3lem  46084  liminfgord  46106  liminflelimsuplem  46127  limsupgtlem  46129  limsupub2  46164  xlimpnfxnegmnf  46166  xlimmnfvlem2  46185  xlimmnfv  46186  xlimpnfvlem2  46189  xlimpnfv  46190  icccncfext  46239  volioc  46324  volico  46335  fourierdlem113  46571  meaiuninclem  46832  meaiuninc3v  46836  icoresmbl  46895  ovolval5lem1  47004  mbfresmf  47091  cnfsmf  47092  incsmf  47094  smfconst  47101  decsmf  47119  smfres  47142  smfco  47154  issmfle2d  47161  finfdm  47198  bgoldbtbndlem3  48161  rrxsphere  49102  i0oii  49273  io1ii  49274