Theorem rexr 11304

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296

This theorem is referenced by:  rexri  11316  lenlt  11336  ltpnf  13159  mnflt  13162  xrltnsym  13175  xrlttr  13178  xrre  13207  xrre3  13209  max1  13223  max2  13225  min1  13227  min2  13228  maxle  13229  lemin  13230  maxlt  13231  ltmin  13232  max0sub  13234  qbtwnxr  13238  xralrple  13243  alrple  13244  xltnegi  13254  rexadd  13270  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  xpncan  13289  xnpcan  13290  xleadd1a  13291  xleadd1  13293  xltadd1  13294  xltadd2  13295  xsubge0  13299  rexmul  13309  xadddilem  13332  xadddir  13334  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  supxrun  13354  supxrunb1  13357  supxrunb2  13358  supxrbnd1  13359  supxrbnd2  13360  xrsup0  13361  supxrbnd  13366  infmremnf  13381  elioo4g  13443  elioc2  13446  elico2  13447  elicc2  13448  iccss  13451  iooshf  13462  iooneg  13507  icoshft  13509  difreicc  13520  hashbnd  14371  elicc4abs  15354  icodiamlt  15470  limsupgord  15504  pcadd  16922  ramubcl  17051  lt6abl  19927  xrsmcmn  21421  xrs1mnd  21439  xrs10  21440  xrsdsreval  21446  psmetge0  24337  xmetge0  24369  imasdsf1olem  24398  bl2in  24425  blssps  24449  blss  24450  blcld  24533  icopnfcld  24803  iocmnfcld  24804  bl2ioo  24827  blssioo  24830  xrtgioo  24841  xrsblre  24846  iccntr  24856  icccmplem2  24858  icccmp  24860  reconnlem2  24862  xrge0tsms  24869  icoopnst  24982  iocopnst  24983  ovolfioo  25515  ovolicc2lem1  25565  ovolicc2lem5  25569  voliunlem3  25600  icombl1  25611  icombl  25612  iccvolcl  25615  ovolioo  25616  ioovolcl  25618  uniiccdif  25626  volsup2  25653  mbfimasn  25680  ismbf3d  25702  mbfsup  25712  itg2seq  25791  bddiblnc  25891  dvlip2  26048  ply1remlem  26218  abelthlem3  26491  abelth  26499  sincosq2sgn  26555  sincosq3sgn  26556  sinq12ge0  26564  sincos6thpi  26572  sineq0  26580  efif1olem1  26598  efif1olem2  26599  efif1o  26602  eff1o  26605  loglesqrt  26818  basellem1  27138  pntlemo  27665  nmobndi  30803  nmopub2tALT  31937  nmfnleub2  31954  nmopcoadji  32129  rexdiv  32892  xrge0tsmsd  33047  pnfneige0  33911  lmxrge0  33912  hashf2  34064  sxbrsigalem0  34252  orvcgteel  34448  orvclteel  34453  sgnclre  34520  sgnneg  34521  signstfvn  34562  signstfvneq0  34565  signsvfn  34575  ivthALT  36317  icorempo  37333  icoreunrn  37341  iooelexlt  37344  relowlssretop  37345  relowlpssretop  37346  poimir  37639  mblfinlem2  37644  iblabsnclem  37669  ftc1anclem1  37679  ftc1anclem6  37684  areacirclem5  37698  areacirc  37699  blbnd  37773  iocmbl  43201  reabssgn  43625  supxrre3  45274  supxrgere  45282  infrpge  45300  infxrunb2  45317  infxrbnd2  45318  infleinflem2  45320  xrralrecnnle  45332  supxrunb3  45348  supminfxr2  45418  xrpnf  45435  ioomidp  45466  limsupre  45596  limsupub  45659  limsuppnflem  45665  limsupre3lem  45687  liminfgord  45709  liminflelimsuplem  45730  limsupgtlem  45732  limsupub2  45767  xlimpnfxnegmnf  45769  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  icccncfext  45842  volioc  45927  volico  45938  fourierdlem113  46174  meaiuninclem  46435  meaiuninc3v  46439  icoresmbl  46498  ovolval5lem1  46607  mbfresmf  46694  cnfsmf  46695  incsmf  46697  smfconst  46704  decsmf  46722  smfres  46745  smfco  46757  issmfle2d  46764  finfdm  46801  bgoldbtbndlem3  47731  rrxsphere  48597  i0oii  48715  io1ii  48716