Theorem rexr 11030

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℝ^*cxr 11017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905  df-xr 11022

This theorem is referenced by:  rexri  11042  lenlt  11062  ltpnf  12865  mnflt  12868  xrltnsym  12880  xrlttr  12883  xrre  12912  xrre3  12914  max1  12928  max2  12930  min1  12932  min2  12933  maxle  12934  lemin  12935  maxlt  12936  ltmin  12937  max0sub  12939  qbtwnxr  12943  xralrple  12948  alrple  12949  xltnegi  12959  rexadd  12975  xaddnemnf  12979  xaddnepnf  12980  xaddcom  12983  xnegdi  12991  xpncan  12994  xnpcan  12995  xleadd1a  12996  xleadd1  12998  xltadd1  12999  xltadd2  13000  xsubge0  13004  rexmul  13014  xadddilem  13037  xadddir  13039  xrsupsslem  13050  xrinfmsslem  13051  xrub  13055  supxrun  13059  supxrunb1  13062  supxrunb2  13063  supxrbnd1  13064  supxrbnd2  13065  xrsup0  13066  supxrbnd  13071  infmremnf  13086  elioo4g  13148  elioc2  13151  elico2  13152  elicc2  13153  iccss  13156  iooshf  13167  iooneg  13212  icoshft  13214  difreicc  13225  hashbnd  14059  elicc4abs  15040  icodiamlt  15156  limsupgord  15190  pcadd  16599  ramubcl  16728  lt6abl  19505  xrsmcmn  20630  xrs1mnd  20645  xrs10  20646  xrsdsreval  20652  psmetge0  23474  xmetge0  23506  imasdsf1olem  23535  bl2in  23562  blssps  23586  blss  23587  blcld  23670  icopnfcld  23940  iocmnfcld  23941  bl2ioo  23964  blssioo  23967  xrtgioo  23978  xrsblre  23983  iccntr  23993  icccmplem2  23995  icccmp  23997  reconnlem2  23999  xrge0tsms  24006  icoopnst  24111  iocopnst  24112  ovolfioo  24640  ovolicc2lem1  24690  ovolicc2lem5  24694  voliunlem3  24725  icombl1  24736  icombl  24737  iccvolcl  24740  ovolioo  24741  ioovolcl  24743  uniiccdif  24751  volsup2  24778  mbfimasn  24805  ismbf3d  24827  mbfsup  24837  itg2seq  24916  bddiblnc  25015  dvlip2  25168  ply1remlem  25336  abelthlem3  25601  abelth  25609  sincosq2sgn  25665  sincosq3sgn  25666  sinq12ge0  25674  sincos6thpi  25681  sineq0  25689  efif1olem1  25707  efif1olem2  25708  efif1o  25711  eff1o  25714  loglesqrt  25920  basellem1  26239  pntlemo  26764  nmobndi  29146  nmopub2tALT  30280  nmfnleub2  30297  nmopcoadji  30472  rexdiv  31209  xrge0tsmsd  31326  pnfneige0  31910  lmxrge0  31911  hashf2  32061  sxbrsigalem0  32247  orvcgteel  32443  orvclteel  32448  sgnclre  32515  sgnneg  32516  signstfvn  32557  signstfvneq0  32560  signsvfn  32570  ivthALT  34533  icorempo  35531  icoreunrn  35539  iooelexlt  35542  relowlssretop  35543  relowlpssretop  35544  poimir  35819  mblfinlem2  35824  iblabsnclem  35849  ftc1anclem1  35859  ftc1anclem6  35864  areacirclem5  35878  areacirc  35879  blbnd  35954  iocmbl  41051  reabssgn  41251  supxrre3  42871  supxrgere  42879  infrpge  42897  infxrunb2  42914  infxrbnd2  42915  infleinflem2  42917  xrralrecnnle  42929  supxrunb3  42946  supminfxr2  43016  xrpnf  43033  ioomidp  43059  limsupre  43189  limsupub  43252  limsuppnflem  43258  limsupre3lem  43280  liminfgord  43302  liminflelimsuplem  43323  limsupgtlem  43325  limsupub2  43360  xlimpnfxnegmnf  43362  xlimmnfvlem2  43381  xlimmnfv  43382  xlimpnfvlem2  43385  xlimpnfv  43386  icccncfext  43435  volioc  43520  volico  43531  fourierdlem113  43767  meaiuninclem  44025  meaiuninc3v  44029  icoresmbl  44088  ovolval5lem1  44197  mbfresmf  44284  cnfsmf  44285  incsmf  44287  smfconst  44294  decsmf  44312  smfres  44335  smfco  44347  issmfle2d  44353  bgoldbtbndlem3  45270  rrxsphere  46105  i0oii  46224  io1ii  46225