Theorem rexr 11182

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℝ^*cxr 11169

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-xr 11174

This theorem is referenced by:  rexri  11194  lenlt  11215  ltpnf  13062  mnflt  13065  xrltnsym  13079  xrlttr  13082  xrre  13112  xrre3  13114  max1  13128  max2  13130  min1  13132  min2  13133  maxle  13134  lemin  13135  maxlt  13136  ltmin  13137  max0sub  13139  qbtwnxr  13143  xralrple  13148  alrple  13149  xltnegi  13159  rexadd  13175  xaddnemnf  13179  xaddnepnf  13180  xaddcom  13183  xnegdi  13191  xpncan  13194  xnpcan  13195  xleadd1a  13196  xleadd1  13198  xltadd1  13199  xltadd2  13200  xsubge0  13204  rexmul  13214  xadddilem  13237  xadddir  13239  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxrun  13259  supxrunb1  13262  supxrunb2  13263  supxrbnd1  13264  supxrbnd2  13265  xrsup0  13266  supxrbnd  13271  infmremnf  13287  elioo4g  13350  elioc2  13353  elico2  13354  elicc2  13355  iccss  13358  iooshf  13370  iooneg  13415  icoshft  13417  difreicc  13428  hashbnd  14289  elicc4abs  15273  icodiamlt  15391  limsupgord  15425  pcadd  16851  ramubcl  16980  lt6abl  19861  xrsmcmn  21381  xrsdsreval  21401  xrs1mnd  21430  xrs10  21431  psmetge0  24287  xmetge0  24319  imasdsf1olem  24348  bl2in  24375  blssps  24399  blss  24400  blcld  24480  icopnfcld  24742  iocmnfcld  24743  bl2ioo  24767  blssioo  24770  xrtgioo  24782  xrsblre  24787  iccntr  24797  icccmplem2  24799  icccmp  24801  reconnlem2  24803  xrge0tsms  24810  icoopnst  24916  iocopnst  24917  ovolfioo  25444  ovolicc2lem1  25494  ovolicc2lem5  25498  voliunlem3  25529  icombl1  25540  icombl  25541  iccvolcl  25544  ovolioo  25545  ioovolcl  25547  uniiccdif  25555  volsup2  25582  mbfimasn  25609  ismbf3d  25631  mbfsup  25641  itg2seq  25719  bddiblnc  25819  dvlip2  25972  ply1remlem  26140  abelthlem3  26411  abelth  26419  sincosq2sgn  26476  sincosq3sgn  26477  sinq12ge0  26485  sincos6thpi  26493  sineq0  26501  efif1olem1  26519  efif1olem2  26520  efif1o  26523  eff1o  26526  loglesqrt  26738  basellem1  27058  pntlemo  27584  nmobndi  30861  nmopub2tALT  31995  nmfnleub2  32012  nmopcoadji  32187  sgnclre  32920  sgnneg  32921  rexdiv  33000  xrge0tsmsd  33149  pnfneige0  34111  lmxrge0  34112  hashf2  34244  sxbrsigalem0  34431  orvcgteel  34628  orvclteel  34633  signstfvn  34729  signstfvneq0  34732  signsvfn  34742  ivthALT  36533  icorempo  37681  icoreunrn  37689  iooelexlt  37692  relowlssretop  37693  relowlpssretop  37694  poimir  37988  mblfinlem2  37993  iblabsnclem  38018  ftc1anclem1  38028  ftc1anclem6  38033  areacirclem5  38047  areacirc  38048  blbnd  38122  iocmbl  43659  reabssgn  44081  supxrre3  45773  supxrgere  45781  infrpge  45799  infxrunb2  45815  infxrbnd2  45816  infleinflem2  45818  xrralrecnnle  45830  supxrunb3  45846  supminfxr2  45915  xrpnf  45931  ioomidp  45962  limsupre  46087  limsupub  46150  limsuppnflem  46156  limsupre3lem  46178  liminfgord  46200  liminflelimsuplem  46221  limsupgtlem  46223  limsupub2  46258  xlimpnfxnegmnf  46260  xlimmnfvlem2  46279  xlimmnfv  46280  xlimpnfvlem2  46283  xlimpnfv  46284  icccncfext  46333  volioc  46418  volico  46429  fourierdlem113  46665  meaiuninclem  46926  meaiuninc3v  46930  icoresmbl  46989  ovolval5lem1  47098  mbfresmf  47185  cnfsmf  47186  incsmf  47188  smfconst  47195  decsmf  47213  smfres  47236  smfco  47248  issmfle2d  47255  finfdm  47292  bgoldbtbndlem3  48295  rrxsphere  49236  i0oii  49407  io1ii  49408