Theorem rexr 11189

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-xr 11181

This theorem is referenced by:  rexri  11201  lenlt  11222  ltpnf  13069  mnflt  13072  xrltnsym  13086  xrlttr  13089  xrre  13119  xrre3  13121  max1  13135  max2  13137  min1  13139  min2  13140  maxle  13141  lemin  13142  maxlt  13143  ltmin  13144  max0sub  13146  qbtwnxr  13150  xralrple  13155  alrple  13156  xltnegi  13166  rexadd  13182  xaddnemnf  13186  xaddnepnf  13187  xaddcom  13190  xnegdi  13198  xpncan  13201  xnpcan  13202  xleadd1a  13203  xleadd1  13205  xltadd1  13206  xltadd2  13207  xsubge0  13211  rexmul  13221  xadddilem  13244  xadddir  13246  xrsupsslem  13257  xrinfmsslem  13258  xrub  13262  supxrun  13266  supxrunb1  13269  supxrunb2  13270  supxrbnd1  13271  supxrbnd2  13272  xrsup0  13273  supxrbnd  13278  infmremnf  13294  elioo4g  13357  elioc2  13360  elico2  13361  elicc2  13362  iccss  13365  iooshf  13377  iooneg  13422  icoshft  13424  difreicc  13435  hashbnd  14296  elicc4abs  15280  icodiamlt  15398  limsupgord  15432  pcadd  16858  ramubcl  16987  lt6abl  19868  xrsmcmn  21377  xrsdsreval  21394  xrs1mnd  21422  xrs10  21423  psmetge0  24302  xmetge0  24334  imasdsf1olem  24363  bl2in  24390  blssps  24414  blss  24415  blcld  24495  icopnfcld  24757  iocmnfcld  24758  bl2ioo  24782  blssioo  24785  xrtgioo  24797  xrsblre  24802  iccntr  24812  icccmplem2  24814  icccmp  24816  reconnlem2  24818  xrge0tsms  24825  icoopnst  24931  iocopnst  24932  ovolfioo  25459  ovolicc2lem1  25509  ovolicc2lem5  25513  voliunlem3  25544  icombl1  25555  icombl  25556  iccvolcl  25559  ovolioo  25560  ioovolcl  25562  uniiccdif  25570  volsup2  25597  mbfimasn  25624  ismbf3d  25646  mbfsup  25656  itg2seq  25734  bddiblnc  25834  dvlip2  25987  ply1remlem  26155  abelthlem3  26423  abelth  26431  sincosq2sgn  26488  sincosq3sgn  26489  sinq12ge0  26497  sincos6thpi  26505  sineq0  26513  efif1olem1  26531  efif1olem2  26532  efif1o  26535  eff1o  26538  loglesqrt  26750  basellem1  27069  pntlemo  27595  nmobndi  30871  nmopub2tALT  32005  nmfnleub2  32022  nmopcoadji  32197  sgnclre  32931  sgnneg  32932  rexdiv  33011  xrge0tsmsd  33161  pnfneige0  34142  lmxrge0  34143  hashf2  34275  sxbrsigalem0  34462  orvcgteel  34659  orvclteel  34664  signstfvn  34760  signstfvneq0  34763  signsvfn  34773  ivthALT  36570  icorempo  37720  icoreunrn  37728  iooelexlt  37731  relowlssretop  37732  relowlpssretop  37733  poimir  38027  mblfinlem2  38032  iblabsnclem  38057  ftc1anclem1  38067  ftc1anclem6  38072  areacirclem5  38086  areacirc  38087  blbnd  38161  iocmbl  43665  reabssgn  44087  supxrre3  45777  supxrgere  45785  infrpge  45803  infxrunb2  45819  infxrbnd2  45820  infleinflem2  45822  xrralrecnnle  45834  supxrunb3  45850  supminfxr2  45919  xrpnf  45935  ioomidp  45966  limsupre  46091  limsupub  46154  limsuppnflem  46160  limsupre3lem  46182  liminfgord  46204  liminflelimsuplem  46225  limsupgtlem  46227  limsupub2  46262  xlimpnfxnegmnf  46264  xlimmnfvlem2  46283  xlimmnfv  46284  xlimpnfvlem2  46287  xlimpnfv  46288  icccncfext  46337  volioc  46422  volico  46433  fourierdlem113  46669  meaiuninclem  46930  meaiuninc3v  46934  icoresmbl  46993  ovolval5lem1  47102  mbfresmf  47189  cnfsmf  47190  incsmf  47192  smfconst  47199  decsmf  47217  smfres  47240  smfco  47252  issmfle2d  47259  finfdm  47296  bgoldbtbndlem3  48305  rrxsphere  49246  i0oii  49417  io1ii  49418