Theorem rexr 11227

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℝ^*cxr 11214

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219

This theorem is referenced by:  rexri  11239  lenlt  11259  ltpnf  13087  mnflt  13090  xrltnsym  13104  xrlttr  13107  xrre  13136  xrre3  13138  max1  13152  max2  13154  min1  13156  min2  13157  maxle  13158  lemin  13159  maxlt  13160  ltmin  13161  max0sub  13163  qbtwnxr  13167  xralrple  13172  alrple  13173  xltnegi  13183  rexadd  13199  xaddnemnf  13203  xaddnepnf  13204  xaddcom  13207  xnegdi  13215  xpncan  13218  xnpcan  13219  xleadd1a  13220  xleadd1  13222  xltadd1  13223  xltadd2  13224  xsubge0  13228  rexmul  13238  xadddilem  13261  xadddir  13263  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  supxrun  13283  supxrunb1  13286  supxrunb2  13287  supxrbnd1  13288  supxrbnd2  13289  xrsup0  13290  supxrbnd  13295  infmremnf  13311  elioo4g  13374  elioc2  13377  elico2  13378  elicc2  13379  iccss  13382  iooshf  13394  iooneg  13439  icoshft  13441  difreicc  13452  hashbnd  14308  elicc4abs  15293  icodiamlt  15411  limsupgord  15445  pcadd  16867  ramubcl  16996  lt6abl  19832  xrsmcmn  21310  xrs1mnd  21328  xrs10  21329  xrsdsreval  21335  psmetge0  24207  xmetge0  24239  imasdsf1olem  24268  bl2in  24295  blssps  24319  blss  24320  blcld  24400  icopnfcld  24662  iocmnfcld  24663  bl2ioo  24687  blssioo  24690  xrtgioo  24702  xrsblre  24707  iccntr  24717  icccmplem2  24719  icccmp  24721  reconnlem2  24723  xrge0tsms  24730  icoopnst  24843  iocopnst  24844  ovolfioo  25375  ovolicc2lem1  25425  ovolicc2lem5  25429  voliunlem3  25460  icombl1  25471  icombl  25472  iccvolcl  25475  ovolioo  25476  ioovolcl  25478  uniiccdif  25486  volsup2  25513  mbfimasn  25540  ismbf3d  25562  mbfsup  25572  itg2seq  25650  bddiblnc  25750  dvlip2  25907  ply1remlem  26077  abelthlem3  26350  abelth  26358  sincosq2sgn  26415  sincosq3sgn  26416  sinq12ge0  26424  sincos6thpi  26432  sineq0  26440  efif1olem1  26458  efif1olem2  26459  efif1o  26462  eff1o  26465  loglesqrt  26678  basellem1  26998  pntlemo  27525  nmobndi  30711  nmopub2tALT  31845  nmfnleub2  31862  nmopcoadji  32037  sgnclre  32764  sgnneg  32765  rexdiv  32853  xrge0tsmsd  33009  pnfneige0  33948  lmxrge0  33949  hashf2  34081  sxbrsigalem0  34269  orvcgteel  34466  orvclteel  34471  signstfvn  34567  signstfvneq0  34570  signsvfn  34580  ivthALT  36330  icorempo  37346  icoreunrn  37354  iooelexlt  37357  relowlssretop  37358  relowlpssretop  37359  poimir  37654  mblfinlem2  37659  iblabsnclem  37684  ftc1anclem1  37694  ftc1anclem6  37699  areacirclem5  37713  areacirc  37714  blbnd  37788  iocmbl  43209  reabssgn  43632  supxrre3  45328  supxrgere  45336  infrpge  45354  infxrunb2  45371  infxrbnd2  45372  infleinflem2  45374  xrralrecnnle  45386  supxrunb3  45402  supminfxr2  45472  xrpnf  45488  ioomidp  45519  limsupre  45646  limsupub  45709  limsuppnflem  45715  limsupre3lem  45737  liminfgord  45759  liminflelimsuplem  45780  limsupgtlem  45782  limsupub2  45817  xlimpnfxnegmnf  45819  xlimmnfvlem2  45838  xlimmnfv  45839  xlimpnfvlem2  45842  xlimpnfv  45843  icccncfext  45892  volioc  45977  volico  45988  fourierdlem113  46224  meaiuninclem  46485  meaiuninc3v  46489  icoresmbl  46548  ovolval5lem1  46657  mbfresmf  46744  cnfsmf  46745  incsmf  46747  smfconst  46754  decsmf  46772  smfres  46795  smfco  46807  issmfle2d  46814  finfdm  46851  bgoldbtbndlem3  47812  rrxsphere  48741  i0oii  48912  io1ii  48913