Theorem rexr 11180

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℝ^*cxr 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-xr 11172

This theorem is referenced by:  rexri  11192  lenlt  11212  ltpnf  13040  mnflt  13043  xrltnsym  13057  xrlttr  13060  xrre  13089  xrre3  13091  max1  13105  max2  13107  min1  13109  min2  13110  maxle  13111  lemin  13112  maxlt  13113  ltmin  13114  max0sub  13116  qbtwnxr  13120  xralrple  13125  alrple  13126  xltnegi  13136  rexadd  13152  xaddnemnf  13156  xaddnepnf  13157  xaddcom  13160  xnegdi  13168  xpncan  13171  xnpcan  13172  xleadd1a  13173  xleadd1  13175  xltadd1  13176  xltadd2  13177  xsubge0  13181  rexmul  13191  xadddilem  13214  xadddir  13216  xrsupsslem  13227  xrinfmsslem  13228  xrub  13232  supxrun  13236  supxrunb1  13239  supxrunb2  13240  supxrbnd1  13241  supxrbnd2  13242  xrsup0  13243  supxrbnd  13248  infmremnf  13264  elioo4g  13327  elioc2  13330  elico2  13331  elicc2  13332  iccss  13335  iooshf  13347  iooneg  13392  icoshft  13394  difreicc  13405  hashbnd  14261  elicc4abs  15245  icodiamlt  15363  limsupgord  15397  pcadd  16819  ramubcl  16948  lt6abl  19792  xrsmcmn  21316  xrsdsreval  21336  xrs1mnd  21365  xrs10  21366  psmetge0  24216  xmetge0  24248  imasdsf1olem  24277  bl2in  24304  blssps  24328  blss  24329  blcld  24409  icopnfcld  24671  iocmnfcld  24672  bl2ioo  24696  blssioo  24699  xrtgioo  24711  xrsblre  24716  iccntr  24726  icccmplem2  24728  icccmp  24730  reconnlem2  24732  xrge0tsms  24739  icoopnst  24852  iocopnst  24853  ovolfioo  25384  ovolicc2lem1  25434  ovolicc2lem5  25438  voliunlem3  25469  icombl1  25480  icombl  25481  iccvolcl  25484  ovolioo  25485  ioovolcl  25487  uniiccdif  25495  volsup2  25522  mbfimasn  25549  ismbf3d  25571  mbfsup  25581  itg2seq  25659  bddiblnc  25759  dvlip2  25916  ply1remlem  26086  abelthlem3  26359  abelth  26367  sincosq2sgn  26424  sincosq3sgn  26425  sinq12ge0  26433  sincos6thpi  26441  sineq0  26449  efif1olem1  26467  efif1olem2  26468  efif1o  26471  eff1o  26474  loglesqrt  26687  basellem1  27007  pntlemo  27534  nmobndi  30737  nmopub2tALT  31871  nmfnleub2  31888  nmopcoadji  32063  sgnclre  32790  sgnneg  32791  rexdiv  32879  xrge0tsmsd  33028  pnfneige0  33917  lmxrge0  33918  hashf2  34050  sxbrsigalem0  34238  orvcgteel  34435  orvclteel  34440  signstfvn  34536  signstfvneq0  34539  signsvfn  34549  ivthALT  36308  icorempo  37324  icoreunrn  37332  iooelexlt  37335  relowlssretop  37336  relowlpssretop  37337  poimir  37632  mblfinlem2  37637  iblabsnclem  37662  ftc1anclem1  37672  ftc1anclem6  37677  areacirclem5  37691  areacirc  37692  blbnd  37766  iocmbl  43186  reabssgn  43609  supxrre3  45305  supxrgere  45313  infrpge  45331  infxrunb2  45348  infxrbnd2  45349  infleinflem2  45351  xrralrecnnle  45363  supxrunb3  45379  supminfxr2  45449  xrpnf  45465  ioomidp  45496  limsupre  45623  limsupub  45686  limsuppnflem  45692  limsupre3lem  45714  liminfgord  45736  liminflelimsuplem  45757  limsupgtlem  45759  limsupub2  45794  xlimpnfxnegmnf  45796  xlimmnfvlem2  45815  xlimmnfv  45816  xlimpnfvlem2  45819  xlimpnfv  45820  icccncfext  45869  volioc  45954  volico  45965  fourierdlem113  46201  meaiuninclem  46462  meaiuninc3v  46466  icoresmbl  46525  ovolval5lem1  46634  mbfresmf  46721  cnfsmf  46722  incsmf  46724  smfconst  46731  decsmf  46749  smfres  46772  smfco  46784  issmfle2d  46791  finfdm  46828  bgoldbtbndlem3  47792  rrxsphere  48734  i0oii  48905  io1ii  48906