Theorem rexr 11301

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

Syntax hints:   → wi 4   ∈ wcel 2099  ℝcr 11148  ℝ^*cxr 11288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3951  df-ss 3963  df-xr 11293

This theorem is referenced by:  rexri  11313  lenlt  11333  ltpnf  13148  mnflt  13151  xrltnsym  13164  xrlttr  13167  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  13370  elioo4g  13432  elioc2  13435  elico2  13436  elicc2  13437  iccss  13440  iooshf  13451  iooneg  13496  icoshft  13498  difreicc  13509  hashbnd  14348  elicc4abs  15319  icodiamlt  15435  limsupgord  15469  pcadd  16886  ramubcl  17015  lt6abl  19889  xrsmcmn  21379  xrs1mnd  21397  xrs10  21398  xrsdsreval  21404  psmetge0  24306  xmetge0  24338  imasdsf1olem  24367  bl2in  24394  blssps  24418  blss  24419  blcld  24502  icopnfcld  24772  iocmnfcld  24773  bl2ioo  24796  blssioo  24799  xrtgioo  24810  xrsblre  24815  iccntr  24825  icccmplem2  24827  icccmp  24829  reconnlem2  24831  xrge0tsms  24838  icoopnst  24951  iocopnst  24952  ovolfioo  25484  ovolicc2lem1  25534  ovolicc2lem5  25538  voliunlem3  25569  icombl1  25580  icombl  25581  iccvolcl  25584  ovolioo  25585  ioovolcl  25587  uniiccdif  25595  volsup2  25622  mbfimasn  25649  ismbf3d  25671  mbfsup  25681  itg2seq  25760  bddiblnc  25859  dvlip2  26016  ply1remlem  26189  abelthlem3  26460  abelth  26468  sincosq2sgn  26524  sincosq3sgn  26525  sinq12ge0  26533  sincos6thpi  26540  sineq0  26548  efif1olem1  26566  efif1olem2  26567  efif1o  26570  eff1o  26573  loglesqrt  26786  basellem1  27106  pntlemo  27633  nmobndi  30705  nmopub2tALT  31839  nmfnleub2  31856  nmopcoadji  32031  rexdiv  32790  xrge0tsmsd  32930  pnfneige0  33779  lmxrge0  33780  hashf2  33930  sxbrsigalem0  34118  orvcgteel  34314  orvclteel  34319  sgnclre  34386  sgnneg  34387  signstfvn  34428  signstfvneq0  34431  signsvfn  34441  ivthALT  36060  icorempo  37071  icoreunrn  37079  iooelexlt  37082  relowlssretop  37083  relowlpssretop  37084  poimir  37367  mblfinlem2  37372  iblabsnclem  37397  ftc1anclem1  37407  ftc1anclem6  37412  areacirclem5  37426  areacirc  37427  blbnd  37501  iocmbl  42915  reabssgn  43340  supxrre3  44976  supxrgere  44984  infrpge  45002  infxrunb2  45019  infxrbnd2  45020  infleinflem2  45022  xrralrecnnle  45034  supxrunb3  45050  supminfxr2  45120  xrpnf  45137  ioomidp  45168  limsupre  45298  limsupub  45361  limsuppnflem  45367  limsupre3lem  45389  liminfgord  45411  liminflelimsuplem  45432  limsupgtlem  45434  limsupub2  45469  xlimpnfxnegmnf  45471  xlimmnfvlem2  45490  xlimmnfv  45491  xlimpnfvlem2  45494  xlimpnfv  45495  icccncfext  45544  volioc  45629  volico  45640  fourierdlem113  45876  meaiuninclem  46137  meaiuninc3v  46141  icoresmbl  46200  ovolval5lem1  46309  mbfresmf  46396  cnfsmf  46397  incsmf  46399  smfconst  46406  decsmf  46424  smfres  46447  smfco  46459  issmfle2d  46466  finfdm  46503  bgoldbtbndlem3  47415  rrxsphere  48172  i0oii  48289  io1ii  48290