Theorem rexr 11259

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 11108  ℝ^*cxr 11246

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-xr 11251

This theorem is referenced by:  rexri  11271  lenlt  11291  ltpnf  13099  mnflt  13102  xrltnsym  13115  xrlttr  13118  xrre  13147  xrre3  13149  max1  13163  max2  13165  min1  13167  min2  13168  maxle  13169  lemin  13170  maxlt  13171  ltmin  13172  max0sub  13174  qbtwnxr  13178  xralrple  13183  alrple  13184  xltnegi  13194  rexadd  13210  xaddnemnf  13214  xaddnepnf  13215  xaddcom  13218  xnegdi  13226  xpncan  13229  xnpcan  13230  xleadd1a  13231  xleadd1  13233  xltadd1  13234  xltadd2  13235  xsubge0  13239  rexmul  13249  xadddilem  13272  xadddir  13274  xrsupsslem  13285  xrinfmsslem  13286  xrub  13290  supxrun  13294  supxrunb1  13297  supxrunb2  13298  supxrbnd1  13299  supxrbnd2  13300  xrsup0  13301  supxrbnd  13306  infmremnf  13321  elioo4g  13383  elioc2  13386  elico2  13387  elicc2  13388  iccss  13391  iooshf  13402  iooneg  13447  icoshft  13449  difreicc  13460  hashbnd  14295  elicc4abs  15265  icodiamlt  15381  limsupgord  15415  pcadd  16821  ramubcl  16950  lt6abl  19762  xrsmcmn  20967  xrs1mnd  20982  xrs10  20983  xrsdsreval  20989  psmetge0  23817  xmetge0  23849  imasdsf1olem  23878  bl2in  23905  blssps  23929  blss  23930  blcld  24013  icopnfcld  24283  iocmnfcld  24284  bl2ioo  24307  blssioo  24310  xrtgioo  24321  xrsblre  24326  iccntr  24336  icccmplem2  24338  icccmp  24340  reconnlem2  24342  xrge0tsms  24349  icoopnst  24454  iocopnst  24455  ovolfioo  24983  ovolicc2lem1  25033  ovolicc2lem5  25037  voliunlem3  25068  icombl1  25079  icombl  25080  iccvolcl  25083  ovolioo  25084  ioovolcl  25086  uniiccdif  25094  volsup2  25121  mbfimasn  25148  ismbf3d  25170  mbfsup  25180  itg2seq  25259  bddiblnc  25358  dvlip2  25511  ply1remlem  25679  abelthlem3  25944  abelth  25952  sincosq2sgn  26008  sincosq3sgn  26009  sinq12ge0  26017  sincos6thpi  26024  sineq0  26032  efif1olem1  26050  efif1olem2  26051  efif1o  26054  eff1o  26057  loglesqrt  26263  basellem1  26582  pntlemo  27107  nmobndi  30023  nmopub2tALT  31157  nmfnleub2  31174  nmopcoadji  31349  rexdiv  32087  xrge0tsmsd  32204  pnfneige0  32926  lmxrge0  32927  hashf2  33077  sxbrsigalem0  33265  orvcgteel  33461  orvclteel  33466  sgnclre  33533  sgnneg  33534  signstfvn  33575  signstfvneq0  33578  signsvfn  33588  ivthALT  35215  icorempo  36227  icoreunrn  36235  iooelexlt  36238  relowlssretop  36239  relowlpssretop  36240  poimir  36516  mblfinlem2  36521  iblabsnclem  36546  ftc1anclem1  36556  ftc1anclem6  36561  areacirclem5  36575  areacirc  36576  blbnd  36650  iocmbl  41952  reabssgn  42377  supxrre3  44025  supxrgere  44033  infrpge  44051  infxrunb2  44068  infxrbnd2  44069  infleinflem2  44071  xrralrecnnle  44083  supxrunb3  44099  supminfxr2  44169  xrpnf  44186  ioomidp  44217  limsupre  44347  limsupub  44410  limsuppnflem  44416  limsupre3lem  44438  liminfgord  44460  liminflelimsuplem  44481  limsupgtlem  44483  limsupub2  44518  xlimpnfxnegmnf  44520  xlimmnfvlem2  44539  xlimmnfv  44540  xlimpnfvlem2  44543  xlimpnfv  44544  icccncfext  44593  volioc  44678  volico  44689  fourierdlem113  44925  meaiuninclem  45186  meaiuninc3v  45190  icoresmbl  45249  ovolval5lem1  45358  mbfresmf  45445  cnfsmf  45446  incsmf  45448  smfconst  45455  decsmf  45473  smfres  45496  smfco  45508  issmfle2d  45515  finfdm  45552  bgoldbtbndlem3  46465  rrxsphere  47424  i0oii  47542  io1ii  47543