Theorem rexr 11243

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-xr 11235

This theorem is referenced by:  rexri  11255  lenlt  11276  ltpnf  13136  mnflt  13139  xrltnsym  13153  xrlttr  13156  xrre  13186  xrre3  13188  max1  13202  max2  13204  min1  13206  min2  13207  maxle  13208  lemin  13209  maxlt  13210  ltmin  13211  max0sub  13213  qbtwnxr  13217  xralrple  13222  alrple  13223  xltnegi  13233  rexadd  13249  xaddnemnf  13253  xaddnepnf  13254  xaddcom  13257  xnegdi  13265  xpncan  13268  xnpcan  13269  xleadd1a  13270  xleadd1  13272  xltadd1  13273  xltadd2  13274  xsubge0  13278  rexmul  13288  xadddilem  13311  xadddir  13313  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  supxrun  13333  supxrunb1  13336  supxrunb2  13337  supxrbnd1  13338  supxrbnd2  13339  xrsup0  13340  supxrbnd  13345  infmremnf  13361  elioo4g  13424  elioc2  13427  elico2  13428  elicc2  13429  iccss  13432  iooshf  13444  iooneg  13489  icoshft  13491  difreicc  13502  hashbnd  14363  sgnneg  15127  sgnclre  15129  elicc4abs  15361  icodiamlt  15479  limsupgord  15513  pcadd  16939  ramubcl  17068  lt6abl  19956  xrsmcmn  21505  xrsdsreval  21522  xrs1mnd  21550  xrs10  21551  psmetge0  24430  xmetge0  24462  imasdsf1olem  24491  bl2in  24518  blssps  24542  blss  24543  blcld  24623  icopnfcld  24885  iocmnfcld  24886  bl2ioo  24910  blssioo  24913  xrtgioo  24925  xrsblre  24930  iccntr  24940  icccmplem2  24942  icccmp  24944  reconnlem2  24946  xrge0tsms  24953  icoopnst  25059  iocopnst  25060  ovolfioo  25587  ovolicc2lem1  25637  ovolicc2lem5  25641  voliunlem3  25672  icombl1  25683  icombl  25684  iccvolcl  25687  ovolioo  25688  ioovolcl  25690  uniiccdif  25698  volsup2  25725  mbfimasn  25752  ismbf3d  25774  mbfsup  25784  itg2seq  25862  bddiblnc  25962  dvlip2  26115  ply1remlem  26283  abelthlem3  26554  abelth  26562  sincosq2sgn  26622  sincosq3sgn  26623  sinq12ge0  26631  sincos6thpi  26639  sineq0  26647  efif1olem1  26665  efif1olem2  26666  efif1o  26669  eff1o  26672  loglesqrt  26884  basellem1  27203  pntlemo  27729  nmobndi  31036  nmopub2tALT  32170  nmfnleub2  32187  nmopcoadji  32362  rexdiv  33158  xrge0tsmsd  33306  pnfneige0  34258  lmxrge0  34259  hashf2  34391  sxbrsigalem0  34578  orvcgteel  34775  orvclteel  34780  signstfvn  34873  signstfvneq0  34876  signsvfn  34886  ivthALT  36708  icorempo  37857  icoreunrn  37865  iooelexlt  37868  relowlssretop  37869  relowlpssretop  37870  poimir  38164  mblfinlem2  38169  iblabsnclem  38194  ftc1anclem1  38204  ftc1anclem6  38209  areacirclem5  38223  areacirc  38224  blbnd  38298  iocmbl  43802  reabssgn  44224  supxrre3  45899  supxrgere  45907  infrpge  45925  infxrunb2  45941  infxrbnd2  45942  infleinflem2  45944  xrralrecnnle  45956  supxrunb3  45972  supminfxr2  46041  xrpnf  46057  ioomidp  46088  limsupre  46213  limsupub  46276  limsuppnflem  46282  limsupre3lem  46304  liminfgord  46326  liminflelimsuplem  46347  limsupgtlem  46349  limsupub2  46384  xlimpnfxnegmnf  46386  xlimmnfvlem2  46405  xlimmnfv  46406  xlimpnfvlem2  46409  xlimpnfv  46410  icccncfext  46459  volioc  46544  volico  46555  fourierdlem113  46791  meaiuninclem  47052  meaiuninc3v  47056  icoresmbl  47115  ovolval5lem1  47224  mbfresmf  47311  cnfsmf  47312  incsmf  47314  smfconst  47321  decsmf  47339  smfres  47362  smfco  47374  issmfle2d  47381  finfdm  47418  bgoldbtbndlem3  48427  rrxsphere  49379  i0oii  49549  io1ii  49550