Theorem rexr 11155

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11002  ℝ^*cxr 11142

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-xr 11147

This theorem is referenced by:  rexri  11167  lenlt  11188  ltpnf  13016  mnflt  13019  xrltnsym  13033  xrlttr  13036  xrre  13065  xrre3  13067  max1  13081  max2  13083  min1  13085  min2  13086  maxle  13087  lemin  13088  maxlt  13089  ltmin  13090  max0sub  13092  qbtwnxr  13096  xralrple  13101  alrple  13102  xltnegi  13112  rexadd  13128  xaddnemnf  13132  xaddnepnf  13133  xaddcom  13136  xnegdi  13144  xpncan  13147  xnpcan  13148  xleadd1a  13149  xleadd1  13151  xltadd1  13152  xltadd2  13153  xsubge0  13157  rexmul  13167  xadddilem  13190  xadddir  13192  xrsupsslem  13203  xrinfmsslem  13204  xrub  13208  supxrun  13212  supxrunb1  13215  supxrunb2  13216  supxrbnd1  13217  supxrbnd2  13218  xrsup0  13219  supxrbnd  13224  infmremnf  13240  elioo4g  13303  elioc2  13306  elico2  13307  elicc2  13308  iccss  13311  iooshf  13323  iooneg  13368  icoshft  13370  difreicc  13381  hashbnd  14240  elicc4abs  15224  icodiamlt  15342  limsupgord  15376  pcadd  16798  ramubcl  16927  lt6abl  19805  xrsmcmn  21326  xrsdsreval  21346  xrs1mnd  21375  xrs10  21376  psmetge0  24225  xmetge0  24257  imasdsf1olem  24286  bl2in  24313  blssps  24337  blss  24338  blcld  24418  icopnfcld  24680  iocmnfcld  24681  bl2ioo  24705  blssioo  24708  xrtgioo  24720  xrsblre  24725  iccntr  24735  icccmplem2  24737  icccmp  24739  reconnlem2  24741  xrge0tsms  24748  icoopnst  24861  iocopnst  24862  ovolfioo  25393  ovolicc2lem1  25443  ovolicc2lem5  25447  voliunlem3  25478  icombl1  25489  icombl  25490  iccvolcl  25493  ovolioo  25494  ioovolcl  25496  uniiccdif  25504  volsup2  25531  mbfimasn  25558  ismbf3d  25580  mbfsup  25590  itg2seq  25668  bddiblnc  25768  dvlip2  25925  ply1remlem  26095  abelthlem3  26368  abelth  26376  sincosq2sgn  26433  sincosq3sgn  26434  sinq12ge0  26442  sincos6thpi  26450  sineq0  26458  efif1olem1  26476  efif1olem2  26477  efif1o  26480  eff1o  26483  loglesqrt  26696  basellem1  27016  pntlemo  27543  nmobndi  30750  nmopub2tALT  31884  nmfnleub2  31901  nmopcoadji  32076  sgnclre  32810  sgnneg  32811  rexdiv  32901  xrge0tsmsd  33037  pnfneige0  33959  lmxrge0  33960  hashf2  34092  sxbrsigalem0  34279  orvcgteel  34476  orvclteel  34481  signstfvn  34577  signstfvneq0  34580  signsvfn  34590  ivthALT  36368  icorempo  37384  icoreunrn  37392  iooelexlt  37395  relowlssretop  37396  relowlpssretop  37397  poimir  37692  mblfinlem2  37697  iblabsnclem  37722  ftc1anclem1  37732  ftc1anclem6  37737  areacirclem5  37751  areacirc  37752  blbnd  37826  iocmbl  43245  reabssgn  43668  supxrre3  45363  supxrgere  45371  infrpge  45389  infxrunb2  45405  infxrbnd2  45406  infleinflem2  45408  xrralrecnnle  45420  supxrunb3  45436  supminfxr2  45506  xrpnf  45522  ioomidp  45553  limsupre  45678  limsupub  45741  limsuppnflem  45747  limsupre3lem  45769  liminfgord  45791  liminflelimsuplem  45812  limsupgtlem  45814  limsupub2  45849  xlimpnfxnegmnf  45851  xlimmnfvlem2  45870  xlimmnfv  45871  xlimpnfvlem2  45874  xlimpnfv  45875  icccncfext  45924  volioc  46009  volico  46020  fourierdlem113  46256  meaiuninclem  46517  meaiuninc3v  46521  icoresmbl  46580  ovolval5lem1  46689  mbfresmf  46776  cnfsmf  46777  incsmf  46779  smfconst  46786  decsmf  46804  smfres  46827  smfco  46839  issmfle2d  46846  finfdm  46883  bgoldbtbndlem3  47837  rrxsphere  48779  i0oii  48950  io1ii  48951