Theorem rexr 9964

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957

This theorem is referenced by:  rexri  9976  lenlt  9995  ltpnf  11830  mnflt  11833  xrltnsym  11846  xrlttr  11849  xrre  11874  xrre3  11876  max1  11890  max2  11892  min1  11894  min2  11895  maxle  11896  lemin  11897  maxlt  11898  ltmin  11899  max0sub  11901  qbtwnxr  11905  xralrple  11910  alrple  11911  xltnegi  11921  rexadd  11937  xaddnemnf  11941  xaddnepnf  11942  xaddcom  11945  xnegdi  11950  xpncan  11953  xnpcan  11954  xleadd1a  11955  xleadd1  11957  xltadd1  11958  xltadd2  11959  xsubge0  11963  rexmul  11973  xadddilem  11996  xadddir  11998  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrun  12018  supxrunb1  12021  supxrunb2  12022  supxrbnd1  12023  supxrbnd2  12024  xrsup0  12025  supxrbnd  12030  infmremnf  12044  elioo4g  12105  elioc2  12107  elico2  12108  elicc2  12109  iccss  12112  iooshf  12123  iooneg  12163  icoshft  12165  difreicc  12175  hashbnd  12985  elicc4abs  13907  icodiamlt  14022  limsupgord  14051  pcadd  15431  ramubcl  15560  lt6abl  18119  xrsmcmn  19588  xrs1mnd  19603  xrs10  19604  xrsdsreval  19610  psmetge0  21927  xmetge0  21959  imasdsf1olem  21988  bl2in  22015  blssps  22039  blss  22040  blcld  22120  icopnfcld  22381  iocmnfcld  22382  bl2ioo  22403  blssioo  22406  xrtgioo  22417  xrsblre  22422  iccntr  22432  icccmplem2  22434  icccmp  22436  reconnlem2  22438  xrge0tsms  22445  icoopnst  22546  iocopnst  22547  ovolfioo  23043  ovolicc2lem1  23092  ovolicc2lem5  23096  voliunlem3  23127  icombl1  23138  icombl  23139  iccvolcl  23142  ovolioo  23143  ioovolcl  23144  uniiccdif  23152  volsup2  23179  mbfimasn  23207  ismbf3d  23227  mbfsup  23237  itg2seq  23315  dvlip2  23562  ply1remlem  23726  abelthlem3  23991  abelth  23999  sincosq2sgn  24055  sincosq3sgn  24056  sinq12ge0  24064  sincos6thpi  24071  sineq0  24077  efif1olem1  24092  efif1olem2  24093  efif1o  24096  eff1o  24099  loglesqrt  24299  basellem1  24607  pntlemo  25096  nmobndi  27014  nmopub2tALT  28152  nmfnleub2  28169  nmopcoadji  28344  rexdiv  28965  xrge0tsmsd  29116  pnfneige0  29325  lmxrge0  29326  hashf2  29473  sxbrsigalem0  29660  omssubadd  29689  orvcgteel  29856  orvclteel  29861  sgnclre  29928  sgnneg  29929  signstfvneq0  29975  ivthALT  31500  icorempt2  32375  icoreunrn  32383  iooelexlt  32386  relowlssretop  32387  relowlpssretop  32388  poimir  32612  mblfinlem2  32617  iblabsnclem  32643  bddiblnc  32650  ftc1anclem1  32655  ftc1anclem6  32660  areacirclem5  32674  areacirc  32675  blbnd  32756  iocmbl  36817  supxrre3  38482  supxrgere  38490  infrpge  38508  infxrunb2  38525  infxrbnd2  38526  infleinflem2  38528  xrralrecnnle  38543  ioomidp  38587  limsupre  38708  icccncfext  38773  volioc  38864  volico  38876  fourierdlem113  39112  meaiuninclem  39373  icoresmbl  39433  ovolval5lem1  39542  mbfresmf  39626  cnfsmf  39627  incsmf  39629  smfconst  39636  decsmf  39653  smfres  39675  smfco  39687  bgoldbtbndlem3  40223