Theorem rexr 11256

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 11254	. 2 ⊢ ℝ ⊆ ℝ*
2	1	sseli 3934	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-xr 11248

This theorem is referenced by:  rexri  11268  lenlt  11289  ltpnf  13146  mnflt  13149  xrltnsym  13163  xrlttr  13166  xrre  13196  xrre3  13198  max1  13212  max2  13214  min1  13216  min2  13217  maxle  13218  lemin  13219  maxlt  13220  ltmin  13221  max0sub  13223  qbtwnxr  13227  xralrple  13232  alrple  13233  xltnegi  13243  rexadd  13259  xaddnemnf  13263  xaddnepnf  13264  xaddcom  13267  xnegdi  13275  xpncan  13278  xnpcan  13279  xleadd1a  13280  xleadd1  13282  xltadd1  13283  xltadd2  13284  xsubge0  13288  rexmul  13298  xadddilem  13321  xadddir  13323  xrsupsslem  13334  xrinfmsslem  13335  xrub  13339  supxrun  13343  supxrunb1  13346  supxrunb2  13347  supxrbnd1  13348  supxrbnd2  13349  xrsup0  13350  supxrbnd  13355  infmremnf  13371  elioo4g  13434  elioc2  13437  elico2  13438  elicc2  13439  iccss  13442  iooshf  13454  iooneg  13499  icoshft  13501  difreicc  13512  hashbnd  14374  sgnneg  15139  sgnclre  15141  elicc4abs  15373  icodiamlt  15491  limsupgord  15525  pcadd  16950  ramubcl  17079  lt6abl  19966  xrsmcmn  21526  xrsdsreval  21543  xrs1mnd  21571  xrs10  21572  psmetge0  24450  xmetge0  24482  imasdsf1olem  24511  bl2in  24538  blssps  24562  blss  24563  blcld  24643  icopnfcld  24905  iocmnfcld  24906  bl2ioo  24930  blssioo  24933  xrtgioo  24945  xrsblre  24950  iccntr  24960  icccmplem2  24962  icccmp  24964  reconnlem2  24966  xrge0tsms  24973  icoopnst  25079  iocopnst  25080  ovolfioo  25607  ovolicc2lem1  25657  ovolicc2lem5  25661  voliunlem3  25692  icombl1  25703  icombl  25704  iccvolcl  25707  ovolioo  25708  ioovolcl  25710  uniiccdif  25718  volsup2  25745  mbfimasn  25772  ismbf3d  25794  mbfsup  25804  itg2seq  25882  bddiblnc  25982  dvlip2  26135  ply1remlem  26303  abelthlem3  26574  abelth  26582  sincosq2sgn  26642  sincosq3sgn  26643  sinq12ge0  26651  sincos6thpi  26659  sineq0  26667  efif1olem1  26685  efif1olem2  26686  efif1o  26689  eff1o  26692  loglesqrt  26904  basellem1  27223  pntlemo  27749  nmobndi  31105  nmopub2tALT  32239  nmfnleub2  32256  nmopcoadji  32431  rexdiv  33223  xrge0tsmsd  33371  pnfneige0  34319  lmxrge0  34320  hashf2  34452  sxbrsigalem0  34639  orvcgteel  34836  orvclteel  34841  signstfvn  34934  signstfvneq0  34937  signsvfn  34947  ivthALT  36824  icorempo  37975  icoreunrn  37983  iooelexlt  37986  relowlssretop  37987  relowlpssretop  37988  poimir  38282  mblfinlem2  38287  iblabsnclem  38312  ftc1anclem1  38322  ftc1anclem6  38327  areacirclem5  38341  areacirc  38342  blbnd  38416  iocmbl  43920  reabssgn  44342  supxrre3  46021  supxrgere  46029  infrpge  46047  infxrunb2  46063  infxrbnd2  46064  infleinflem2  46066  xrralrecnnle  46078  supxrunb3  46094  supminfxr2  46163  xrpnf  46179  ioomidp  46210  limsupre  46335  limsupub  46398  limsuppnflem  46404  limsupre3lem  46426  liminfgord  46448  liminflelimsuplem  46469  limsupgtlem  46471  limsupub2  46506  xlimpnfxnegmnf  46508  xlimmnfvlem2  46527  xlimmnfv  46528  xlimpnfvlem2  46531  xlimpnfv  46532  icccncfext  46581  volioc  46666  volico  46677  fourierdlem113  46913  meaiuninclem  47174  meaiuninc3v  47178  icoresmbl  47237  ovolval5lem1  47346  mbfresmf  47433  cnfsmf  47434  incsmf  47436  smfconst  47443  decsmf  47461  smfres  47484  smfco  47496  issmfle2d  47503  finfdm  47540  bgoldbtbndlem3  48549  rrxsphere  49505  i0oii  49675  io1ii  49676