Theorem rexr 11307

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  ℝ^*cxr 11294

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-xr 11299

This theorem is referenced by:  rexri  11319  lenlt  11339  ltpnf  13162  mnflt  13165  xrltnsym  13179  xrlttr  13182  xrre  13211  xrre3  13213  max1  13227  max2  13229  min1  13231  min2  13232  maxle  13233  lemin  13234  maxlt  13235  ltmin  13236  max0sub  13238  qbtwnxr  13242  xralrple  13247  alrple  13248  xltnegi  13258  rexadd  13274  xaddnemnf  13278  xaddnepnf  13279  xaddcom  13282  xnegdi  13290  xpncan  13293  xnpcan  13294  xleadd1a  13295  xleadd1  13297  xltadd1  13298  xltadd2  13299  xsubge0  13303  rexmul  13313  xadddilem  13336  xadddir  13338  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  supxrun  13358  supxrunb1  13361  supxrunb2  13362  supxrbnd1  13363  supxrbnd2  13364  xrsup0  13365  supxrbnd  13370  infmremnf  13385  elioo4g  13447  elioc2  13450  elico2  13451  elicc2  13452  iccss  13455  iooshf  13466  iooneg  13511  icoshft  13513  difreicc  13524  hashbnd  14375  elicc4abs  15358  icodiamlt  15474  limsupgord  15508  pcadd  16927  ramubcl  17056  lt6abl  19913  xrsmcmn  21404  xrs1mnd  21422  xrs10  21423  xrsdsreval  21429  psmetge0  24322  xmetge0  24354  imasdsf1olem  24383  bl2in  24410  blssps  24434  blss  24435  blcld  24518  icopnfcld  24788  iocmnfcld  24789  bl2ioo  24813  blssioo  24816  xrtgioo  24828  xrsblre  24833  iccntr  24843  icccmplem2  24845  icccmp  24847  reconnlem2  24849  xrge0tsms  24856  icoopnst  24969  iocopnst  24970  ovolfioo  25502  ovolicc2lem1  25552  ovolicc2lem5  25556  voliunlem3  25587  icombl1  25598  icombl  25599  iccvolcl  25602  ovolioo  25603  ioovolcl  25605  uniiccdif  25613  volsup2  25640  mbfimasn  25667  ismbf3d  25689  mbfsup  25699  itg2seq  25777  bddiblnc  25877  dvlip2  26034  ply1remlem  26204  abelthlem3  26477  abelth  26485  sincosq2sgn  26541  sincosq3sgn  26542  sinq12ge0  26550  sincos6thpi  26558  sineq0  26566  efif1olem1  26584  efif1olem2  26585  efif1o  26588  eff1o  26591  loglesqrt  26804  basellem1  27124  pntlemo  27651  nmobndi  30794  nmopub2tALT  31928  nmfnleub2  31945  nmopcoadji  32120  rexdiv  32908  xrge0tsmsd  33065  pnfneige0  33950  lmxrge0  33951  hashf2  34085  sxbrsigalem0  34273  orvcgteel  34470  orvclteel  34475  sgnclre  34542  sgnneg  34543  signstfvn  34584  signstfvneq0  34587  signsvfn  34597  ivthALT  36336  icorempo  37352  icoreunrn  37360  iooelexlt  37363  relowlssretop  37364  relowlpssretop  37365  poimir  37660  mblfinlem2  37665  iblabsnclem  37690  ftc1anclem1  37700  ftc1anclem6  37705  areacirclem5  37719  areacirc  37720  blbnd  37794  iocmbl  43225  reabssgn  43649  supxrre3  45336  supxrgere  45344  infrpge  45362  infxrunb2  45379  infxrbnd2  45380  infleinflem2  45382  xrralrecnnle  45394  supxrunb3  45410  supminfxr2  45480  xrpnf  45496  ioomidp  45527  limsupre  45656  limsupub  45719  limsuppnflem  45725  limsupre3lem  45747  liminfgord  45769  liminflelimsuplem  45790  limsupgtlem  45792  limsupub2  45827  xlimpnfxnegmnf  45829  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  icccncfext  45902  volioc  45987  volico  45998  fourierdlem113  46234  meaiuninclem  46495  meaiuninc3v  46499  icoresmbl  46558  ovolval5lem1  46667  mbfresmf  46754  cnfsmf  46755  incsmf  46757  smfconst  46764  decsmf  46782  smfres  46805  smfco  46817  issmfle2d  46824  finfdm  46861  bgoldbtbndlem3  47794  rrxsphere  48669  i0oii  48817  io1ii  48818