Theorem rexr 11260

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  ℝ^*cxr 11247

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252

This theorem is referenced by:  rexri  11272  lenlt  11292  ltpnf  13100  mnflt  13103  xrltnsym  13116  xrlttr  13119  xrre  13148  xrre3  13150  max1  13164  max2  13166  min1  13168  min2  13169  maxle  13170  lemin  13171  maxlt  13172  ltmin  13173  max0sub  13175  qbtwnxr  13179  xralrple  13184  alrple  13185  xltnegi  13195  rexadd  13211  xaddnemnf  13215  xaddnepnf  13216  xaddcom  13219  xnegdi  13227  xpncan  13230  xnpcan  13231  xleadd1a  13232  xleadd1  13234  xltadd1  13235  xltadd2  13236  xsubge0  13240  rexmul  13250  xadddilem  13273  xadddir  13275  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxrun  13295  supxrunb1  13298  supxrunb2  13299  supxrbnd1  13300  supxrbnd2  13301  xrsup0  13302  supxrbnd  13307  infmremnf  13322  elioo4g  13384  elioc2  13387  elico2  13388  elicc2  13389  iccss  13392  iooshf  13403  iooneg  13448  icoshft  13450  difreicc  13461  hashbnd  14296  elicc4abs  15266  icodiamlt  15382  limsupgord  15416  pcadd  16822  ramubcl  16951  lt6abl  19763  xrsmcmn  20968  xrs1mnd  20983  xrs10  20984  xrsdsreval  20990  psmetge0  23818  xmetge0  23850  imasdsf1olem  23879  bl2in  23906  blssps  23930  blss  23931  blcld  24014  icopnfcld  24284  iocmnfcld  24285  bl2ioo  24308  blssioo  24311  xrtgioo  24322  xrsblre  24327  iccntr  24337  icccmplem2  24339  icccmp  24341  reconnlem2  24343  xrge0tsms  24350  icoopnst  24455  iocopnst  24456  ovolfioo  24984  ovolicc2lem1  25034  ovolicc2lem5  25038  voliunlem3  25069  icombl1  25080  icombl  25081  iccvolcl  25084  ovolioo  25085  ioovolcl  25087  uniiccdif  25095  volsup2  25122  mbfimasn  25149  ismbf3d  25171  mbfsup  25181  itg2seq  25260  bddiblnc  25359  dvlip2  25512  ply1remlem  25680  abelthlem3  25945  abelth  25953  sincosq2sgn  26009  sincosq3sgn  26010  sinq12ge0  26018  sincos6thpi  26025  sineq0  26033  efif1olem1  26051  efif1olem2  26052  efif1o  26055  eff1o  26058  loglesqrt  26266  basellem1  26585  pntlemo  27110  nmobndi  30028  nmopub2tALT  31162  nmfnleub2  31179  nmopcoadji  31354  rexdiv  32092  xrge0tsmsd  32209  pnfneige0  32931  lmxrge0  32932  hashf2  33082  sxbrsigalem0  33270  orvcgteel  33466  orvclteel  33471  sgnclre  33538  sgnneg  33539  signstfvn  33580  signstfvneq0  33583  signsvfn  33593  ivthALT  35220  icorempo  36232  icoreunrn  36240  iooelexlt  36243  relowlssretop  36244  relowlpssretop  36245  poimir  36521  mblfinlem2  36526  iblabsnclem  36551  ftc1anclem1  36561  ftc1anclem6  36566  areacirclem5  36580  areacirc  36581  blbnd  36655  iocmbl  41962  reabssgn  42387  supxrre3  44035  supxrgere  44043  infrpge  44061  infxrunb2  44078  infxrbnd2  44079  infleinflem2  44081  xrralrecnnle  44093  supxrunb3  44109  supminfxr2  44179  xrpnf  44196  ioomidp  44227  limsupre  44357  limsupub  44420  limsuppnflem  44426  limsupre3lem  44448  liminfgord  44470  liminflelimsuplem  44491  limsupgtlem  44493  limsupub2  44528  xlimpnfxnegmnf  44530  xlimmnfvlem2  44549  xlimmnfv  44550  xlimpnfvlem2  44553  xlimpnfv  44554  icccncfext  44603  volioc  44688  volico  44699  fourierdlem113  44935  meaiuninclem  45196  meaiuninc3v  45200  icoresmbl  45259  ovolval5lem1  45368  mbfresmf  45455  cnfsmf  45456  incsmf  45458  smfconst  45465  decsmf  45483  smfres  45506  smfco  45518  issmfle2d  45525  finfdm  45562  bgoldbtbndlem3  46475  rrxsphere  47434  i0oii  47552  io1ii  47553