Theorem rexr 11220

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℝ^*cxr 11207

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 3449  df-un 3919  df-ss 3931  df-xr 11212

This theorem is referenced by:  rexri  11232  lenlt  11252  ltpnf  13080  mnflt  13083  xrltnsym  13097  xrlttr  13100  xrre  13129  xrre3  13131  max1  13145  max2  13147  min1  13149  min2  13150  maxle  13151  lemin  13152  maxlt  13153  ltmin  13154  max0sub  13156  qbtwnxr  13160  xralrple  13165  alrple  13166  xltnegi  13176  rexadd  13192  xaddnemnf  13196  xaddnepnf  13197  xaddcom  13200  xnegdi  13208  xpncan  13211  xnpcan  13212  xleadd1a  13213  xleadd1  13215  xltadd1  13216  xltadd2  13217  xsubge0  13221  rexmul  13231  xadddilem  13254  xadddir  13256  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  supxrun  13276  supxrunb1  13279  supxrunb2  13280  supxrbnd1  13281  supxrbnd2  13282  xrsup0  13283  supxrbnd  13288  infmremnf  13304  elioo4g  13367  elioc2  13370  elico2  13371  elicc2  13372  iccss  13375  iooshf  13387  iooneg  13432  icoshft  13434  difreicc  13445  hashbnd  14301  elicc4abs  15286  icodiamlt  15404  limsupgord  15438  pcadd  16860  ramubcl  16989  lt6abl  19825  xrsmcmn  21303  xrs1mnd  21321  xrs10  21322  xrsdsreval  21328  psmetge0  24200  xmetge0  24232  imasdsf1olem  24261  bl2in  24288  blssps  24312  blss  24313  blcld  24393  icopnfcld  24655  iocmnfcld  24656  bl2ioo  24680  blssioo  24683  xrtgioo  24695  xrsblre  24700  iccntr  24710  icccmplem2  24712  icccmp  24714  reconnlem2  24716  xrge0tsms  24723  icoopnst  24836  iocopnst  24837  ovolfioo  25368  ovolicc2lem1  25418  ovolicc2lem5  25422  voliunlem3  25453  icombl1  25464  icombl  25465  iccvolcl  25468  ovolioo  25469  ioovolcl  25471  uniiccdif  25479  volsup2  25506  mbfimasn  25533  ismbf3d  25555  mbfsup  25565  itg2seq  25643  bddiblnc  25743  dvlip2  25900  ply1remlem  26070  abelthlem3  26343  abelth  26351  sincosq2sgn  26408  sincosq3sgn  26409  sinq12ge0  26417  sincos6thpi  26425  sineq0  26433  efif1olem1  26451  efif1olem2  26452  efif1o  26455  eff1o  26458  loglesqrt  26671  basellem1  26991  pntlemo  27518  nmobndi  30704  nmopub2tALT  31838  nmfnleub2  31855  nmopcoadji  32030  sgnclre  32757  sgnneg  32758  rexdiv  32846  xrge0tsmsd  33002  pnfneige0  33941  lmxrge0  33942  hashf2  34074  sxbrsigalem0  34262  orvcgteel  34459  orvclteel  34464  signstfvn  34560  signstfvneq0  34563  signsvfn  34573  ivthALT  36323  icorempo  37339  icoreunrn  37347  iooelexlt  37350  relowlssretop  37351  relowlpssretop  37352  poimir  37647  mblfinlem2  37652  iblabsnclem  37677  ftc1anclem1  37687  ftc1anclem6  37692  areacirclem5  37706  areacirc  37707  blbnd  37781  iocmbl  43202  reabssgn  43625  supxrre3  45321  supxrgere  45329  infrpge  45347  infxrunb2  45364  infxrbnd2  45365  infleinflem2  45367  xrralrecnnle  45379  supxrunb3  45395  supminfxr2  45465  xrpnf  45481  ioomidp  45512  limsupre  45639  limsupub  45702  limsuppnflem  45708  limsupre3lem  45730  liminfgord  45752  liminflelimsuplem  45773  limsupgtlem  45775  limsupub2  45810  xlimpnfxnegmnf  45812  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  icccncfext  45885  volioc  45970  volico  45981  fourierdlem113  46217  meaiuninclem  46478  meaiuninc3v  46482  icoresmbl  46541  ovolval5lem1  46650  mbfresmf  46737  cnfsmf  46738  incsmf  46740  smfconst  46747  decsmf  46765  smfres  46788  smfco  46800  issmfle2d  46807  finfdm  46844  bgoldbtbndlem3  47808  rrxsphere  48737  i0oii  48908  io1ii  48909