Theorem rexr 11336

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328

This theorem is referenced by:  rexri  11348  lenlt  11368  ltpnf  13183  mnflt  13186  xrltnsym  13199  xrlttr  13202  xrre  13231  xrre3  13233  max1  13247  max2  13249  min1  13251  min2  13252  maxle  13253  lemin  13254  maxlt  13255  ltmin  13256  max0sub  13258  qbtwnxr  13262  xralrple  13267  alrple  13268  xltnegi  13278  rexadd  13294  xaddnemnf  13298  xaddnepnf  13299  xaddcom  13302  xnegdi  13310  xpncan  13313  xnpcan  13314  xleadd1a  13315  xleadd1  13317  xltadd1  13318  xltadd2  13319  xsubge0  13323  rexmul  13333  xadddilem  13356  xadddir  13358  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrun  13378  supxrunb1  13381  supxrunb2  13382  supxrbnd1  13383  supxrbnd2  13384  xrsup0  13385  supxrbnd  13390  infmremnf  13405  elioo4g  13467  elioc2  13470  elico2  13471  elicc2  13472  iccss  13475  iooshf  13486  iooneg  13531  icoshft  13533  difreicc  13544  hashbnd  14385  elicc4abs  15368  icodiamlt  15484  limsupgord  15518  pcadd  16936  ramubcl  17065  lt6abl  19937  xrsmcmn  21427  xrs1mnd  21445  xrs10  21446  xrsdsreval  21452  psmetge0  24343  xmetge0  24375  imasdsf1olem  24404  bl2in  24431  blssps  24455  blss  24456  blcld  24539  icopnfcld  24809  iocmnfcld  24810  bl2ioo  24833  blssioo  24836  xrtgioo  24847  xrsblre  24852  iccntr  24862  icccmplem2  24864  icccmp  24866  reconnlem2  24868  xrge0tsms  24875  icoopnst  24988  iocopnst  24989  ovolfioo  25521  ovolicc2lem1  25571  ovolicc2lem5  25575  voliunlem3  25606  icombl1  25617  icombl  25618  iccvolcl  25621  ovolioo  25622  ioovolcl  25624  uniiccdif  25632  volsup2  25659  mbfimasn  25686  ismbf3d  25708  mbfsup  25718  itg2seq  25797  bddiblnc  25897  dvlip2  26054  ply1remlem  26224  abelthlem3  26495  abelth  26503  sincosq2sgn  26559  sincosq3sgn  26560  sinq12ge0  26568  sincos6thpi  26576  sineq0  26584  efif1olem1  26602  efif1olem2  26603  efif1o  26606  eff1o  26609  loglesqrt  26822  basellem1  27142  pntlemo  27669  nmobndi  30807  nmopub2tALT  31941  nmfnleub2  31958  nmopcoadji  32133  rexdiv  32890  xrge0tsmsd  33041  pnfneige0  33897  lmxrge0  33898  hashf2  34048  sxbrsigalem0  34236  orvcgteel  34432  orvclteel  34437  sgnclre  34504  sgnneg  34505  signstfvn  34546  signstfvneq0  34549  signsvfn  34559  ivthALT  36301  icorempo  37317  icoreunrn  37325  iooelexlt  37328  relowlssretop  37329  relowlpssretop  37330  poimir  37613  mblfinlem2  37618  iblabsnclem  37643  ftc1anclem1  37653  ftc1anclem6  37658  areacirclem5  37672  areacirc  37673  blbnd  37747  iocmbl  43174  reabssgn  43598  supxrre3  45240  supxrgere  45248  infrpge  45266  infxrunb2  45283  infxrbnd2  45284  infleinflem2  45286  xrralrecnnle  45298  supxrunb3  45314  supminfxr2  45384  xrpnf  45401  ioomidp  45432  limsupre  45562  limsupub  45625  limsuppnflem  45631  limsupre3lem  45653  liminfgord  45675  liminflelimsuplem  45696  limsupgtlem  45698  limsupub2  45733  xlimpnfxnegmnf  45735  xlimmnfvlem2  45754  xlimmnfv  45755  xlimpnfvlem2  45758  xlimpnfv  45759  icccncfext  45808  volioc  45893  volico  45904  fourierdlem113  46140  meaiuninclem  46401  meaiuninc3v  46405  icoresmbl  46464  ovolval5lem1  46573  mbfresmf  46660  cnfsmf  46661  incsmf  46663  smfconst  46670  decsmf  46688  smfres  46711  smfco  46723  issmfle2d  46730  finfdm  46767  bgoldbtbndlem3  47681  rrxsphere  48482  i0oii  48599  io1ii  48600