Theorem rexr 11165

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  ℝ^*cxr 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-xr 11157

This theorem is referenced by:  rexri  11177  lenlt  11198  ltpnf  13021  mnflt  13024  xrltnsym  13038  xrlttr  13041  xrre  13070  xrre3  13072  max1  13086  max2  13088  min1  13090  min2  13091  maxle  13092  lemin  13093  maxlt  13094  ltmin  13095  max0sub  13097  qbtwnxr  13101  xralrple  13106  alrple  13107  xltnegi  13117  rexadd  13133  xaddnemnf  13137  xaddnepnf  13138  xaddcom  13141  xnegdi  13149  xpncan  13152  xnpcan  13153  xleadd1a  13154  xleadd1  13156  xltadd1  13157  xltadd2  13158  xsubge0  13162  rexmul  13172  xadddilem  13195  xadddir  13197  xrsupsslem  13208  xrinfmsslem  13209  xrub  13213  supxrun  13217  supxrunb1  13220  supxrunb2  13221  supxrbnd1  13222  supxrbnd2  13223  xrsup0  13224  supxrbnd  13229  infmremnf  13245  elioo4g  13308  elioc2  13311  elico2  13312  elicc2  13313  iccss  13316  iooshf  13328  iooneg  13373  icoshft  13375  difreicc  13386  hashbnd  14245  elicc4abs  15229  icodiamlt  15347  limsupgord  15381  pcadd  16803  ramubcl  16932  lt6abl  19809  xrsmcmn  21330  xrsdsreval  21350  xrs1mnd  21379  xrs10  21380  psmetge0  24228  xmetge0  24260  imasdsf1olem  24289  bl2in  24316  blssps  24340  blss  24341  blcld  24421  icopnfcld  24683  iocmnfcld  24684  bl2ioo  24708  blssioo  24711  xrtgioo  24723  xrsblre  24728  iccntr  24738  icccmplem2  24740  icccmp  24742  reconnlem2  24744  xrge0tsms  24751  icoopnst  24864  iocopnst  24865  ovolfioo  25396  ovolicc2lem1  25446  ovolicc2lem5  25450  voliunlem3  25481  icombl1  25492  icombl  25493  iccvolcl  25496  ovolioo  25497  ioovolcl  25499  uniiccdif  25507  volsup2  25534  mbfimasn  25561  ismbf3d  25583  mbfsup  25593  itg2seq  25671  bddiblnc  25771  dvlip2  25928  ply1remlem  26098  abelthlem3  26371  abelth  26379  sincosq2sgn  26436  sincosq3sgn  26437  sinq12ge0  26445  sincos6thpi  26453  sineq0  26461  efif1olem1  26479  efif1olem2  26480  efif1o  26483  eff1o  26486  loglesqrt  26699  basellem1  27019  pntlemo  27546  nmobndi  30757  nmopub2tALT  31891  nmfnleub2  31908  nmopcoadji  32083  sgnclre  32820  sgnneg  32821  rexdiv  32913  xrge0tsmsd  33049  pnfneige0  33985  lmxrge0  33986  hashf2  34118  sxbrsigalem0  34305  orvcgteel  34502  orvclteel  34507  signstfvn  34603  signstfvneq0  34606  signsvfn  34616  ivthALT  36400  icorempo  37416  icoreunrn  37424  iooelexlt  37427  relowlssretop  37428  relowlpssretop  37429  poimir  37713  mblfinlem2  37718  iblabsnclem  37743  ftc1anclem1  37753  ftc1anclem6  37758  areacirclem5  37772  areacirc  37773  blbnd  37847  iocmbl  43330  reabssgn  43753  supxrre3  45448  supxrgere  45456  infrpge  45474  infxrunb2  45490  infxrbnd2  45491  infleinflem2  45493  xrralrecnnle  45505  supxrunb3  45521  supminfxr2  45591  xrpnf  45607  ioomidp  45638  limsupre  45763  limsupub  45826  limsuppnflem  45832  limsupre3lem  45854  liminfgord  45876  liminflelimsuplem  45897  limsupgtlem  45899  limsupub2  45934  xlimpnfxnegmnf  45936  xlimmnfvlem2  45955  xlimmnfv  45956  xlimpnfvlem2  45959  xlimpnfv  45960  icccncfext  46009  volioc  46094  volico  46105  fourierdlem113  46341  meaiuninclem  46602  meaiuninc3v  46606  icoresmbl  46665  ovolval5lem1  46774  mbfresmf  46861  cnfsmf  46862  incsmf  46864  smfconst  46871  decsmf  46889  smfres  46912  smfco  46924  issmfle2d  46931  finfdm  46968  bgoldbtbndlem3  47931  rrxsphere  48873  i0oii  49044  io1ii  49045