Theorem rexr 10844

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℝcr 10693  ℝ^*cxr 10831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-xr 10836

This theorem is referenced by:  rexri  10856  lenlt  10876  ltpnf  12677  mnflt  12680  xrltnsym  12692  xrlttr  12695  xrre  12724  xrre3  12726  max1  12740  max2  12742  min1  12744  min2  12745  maxle  12746  lemin  12747  maxlt  12748  ltmin  12749  max0sub  12751  qbtwnxr  12755  xralrple  12760  alrple  12761  xltnegi  12771  rexadd  12787  xaddnemnf  12791  xaddnepnf  12792  xaddcom  12795  xnegdi  12803  xpncan  12806  xnpcan  12807  xleadd1a  12808  xleadd1  12810  xltadd1  12811  xltadd2  12812  xsubge0  12816  rexmul  12826  xadddilem  12849  xadddir  12851  xrsupsslem  12862  xrinfmsslem  12863  xrub  12867  supxrun  12871  supxrunb1  12874  supxrunb2  12875  supxrbnd1  12876  supxrbnd2  12877  xrsup0  12878  supxrbnd  12883  infmremnf  12898  elioo4g  12960  elioc2  12963  elico2  12964  elicc2  12965  iccss  12968  iooshf  12979  iooneg  13024  icoshft  13026  difreicc  13037  hashbnd  13867  elicc4abs  14848  icodiamlt  14964  limsupgord  14998  pcadd  16405  ramubcl  16534  lt6abl  19234  xrsmcmn  20340  xrs1mnd  20355  xrs10  20356  xrsdsreval  20362  psmetge0  23164  xmetge0  23196  imasdsf1olem  23225  bl2in  23252  blssps  23276  blss  23277  blcld  23357  icopnfcld  23619  iocmnfcld  23620  bl2ioo  23643  blssioo  23646  xrtgioo  23657  xrsblre  23662  iccntr  23672  icccmplem2  23674  icccmp  23676  reconnlem2  23678  xrge0tsms  23685  icoopnst  23790  iocopnst  23791  ovolfioo  24318  ovolicc2lem1  24368  ovolicc2lem5  24372  voliunlem3  24403  icombl1  24414  icombl  24415  iccvolcl  24418  ovolioo  24419  ioovolcl  24421  uniiccdif  24429  volsup2  24456  mbfimasn  24483  ismbf3d  24505  mbfsup  24515  itg2seq  24594  bddiblnc  24693  dvlip2  24846  ply1remlem  25014  abelthlem3  25279  abelth  25287  sincosq2sgn  25343  sincosq3sgn  25344  sinq12ge0  25352  sincos6thpi  25359  sineq0  25367  efif1olem1  25385  efif1olem2  25386  efif1o  25389  eff1o  25392  loglesqrt  25598  basellem1  25917  pntlemo  26442  nmobndi  28810  nmopub2tALT  29944  nmfnleub2  29961  nmopcoadji  30136  rexdiv  30874  xrge0tsmsd  30990  pnfneige0  31569  lmxrge0  31570  hashf2  31718  sxbrsigalem0  31904  orvcgteel  32100  orvclteel  32105  sgnclre  32172  sgnneg  32173  signstfvn  32214  signstfvneq0  32217  signsvfn  32227  ivthALT  34210  icorempo  35208  icoreunrn  35216  iooelexlt  35219  relowlssretop  35220  relowlpssretop  35221  poimir  35496  mblfinlem2  35501  iblabsnclem  35526  ftc1anclem1  35536  ftc1anclem6  35541  areacirclem5  35555  areacirc  35556  blbnd  35631  iocmbl  40688  reabssgn  40861  supxrre3  42478  supxrgere  42486  infrpge  42504  infxrunb2  42521  infxrbnd2  42522  infleinflem2  42524  xrralrecnnle  42536  supxrunb3  42553  supminfxr2  42625  xrpnf  42642  ioomidp  42668  limsupre  42800  limsupub  42863  limsuppnflem  42869  limsupre3lem  42891  liminfgord  42913  liminflelimsuplem  42934  limsupgtlem  42936  limsupub2  42971  xlimpnfxnegmnf  42973  xlimmnfvlem2  42992  xlimmnfv  42993  xlimpnfvlem2  42996  xlimpnfv  42997  icccncfext  43046  volioc  43131  volico  43142  fourierdlem113  43378  meaiuninclem  43636  meaiuninc3v  43640  icoresmbl  43699  ovolval5lem1  43808  mbfresmf  43890  cnfsmf  43891  incsmf  43893  smfconst  43900  decsmf  43917  smfres  43939  smfco  43951  issmfle2d  43957  bgoldbtbndlem3  44875  rrxsphere  45710  i0oii  45829  io1ii  45830