Theorem rexr 10952

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℝ^*cxr 10939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944

This theorem is referenced by:  rexri  10964  lenlt  10984  ltpnf  12785  mnflt  12788  xrltnsym  12800  xrlttr  12803  xrre  12832  xrre3  12834  max1  12848  max2  12850  min1  12852  min2  12853  maxle  12854  lemin  12855  maxlt  12856  ltmin  12857  max0sub  12859  qbtwnxr  12863  xralrple  12868  alrple  12869  xltnegi  12879  rexadd  12895  xaddnemnf  12899  xaddnepnf  12900  xaddcom  12903  xnegdi  12911  xpncan  12914  xnpcan  12915  xleadd1a  12916  xleadd1  12918  xltadd1  12919  xltadd2  12920  xsubge0  12924  rexmul  12934  xadddilem  12957  xadddir  12959  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxrun  12979  supxrunb1  12982  supxrunb2  12983  supxrbnd1  12984  supxrbnd2  12985  xrsup0  12986  supxrbnd  12991  infmremnf  13006  elioo4g  13068  elioc2  13071  elico2  13072  elicc2  13073  iccss  13076  iooshf  13087  iooneg  13132  icoshft  13134  difreicc  13145  hashbnd  13978  elicc4abs  14959  icodiamlt  15075  limsupgord  15109  pcadd  16518  ramubcl  16647  lt6abl  19411  xrsmcmn  20533  xrs1mnd  20548  xrs10  20549  xrsdsreval  20555  psmetge0  23373  xmetge0  23405  imasdsf1olem  23434  bl2in  23461  blssps  23485  blss  23486  blcld  23567  icopnfcld  23837  iocmnfcld  23838  bl2ioo  23861  blssioo  23864  xrtgioo  23875  xrsblre  23880  iccntr  23890  icccmplem2  23892  icccmp  23894  reconnlem2  23896  xrge0tsms  23903  icoopnst  24008  iocopnst  24009  ovolfioo  24536  ovolicc2lem1  24586  ovolicc2lem5  24590  voliunlem3  24621  icombl1  24632  icombl  24633  iccvolcl  24636  ovolioo  24637  ioovolcl  24639  uniiccdif  24647  volsup2  24674  mbfimasn  24701  ismbf3d  24723  mbfsup  24733  itg2seq  24812  bddiblnc  24911  dvlip2  25064  ply1remlem  25232  abelthlem3  25497  abelth  25505  sincosq2sgn  25561  sincosq3sgn  25562  sinq12ge0  25570  sincos6thpi  25577  sineq0  25585  efif1olem1  25603  efif1olem2  25604  efif1o  25607  eff1o  25610  loglesqrt  25816  basellem1  26135  pntlemo  26660  nmobndi  29038  nmopub2tALT  30172  nmfnleub2  30189  nmopcoadji  30364  rexdiv  31102  xrge0tsmsd  31219  pnfneige0  31803  lmxrge0  31804  hashf2  31952  sxbrsigalem0  32138  orvcgteel  32334  orvclteel  32339  sgnclre  32406  sgnneg  32407  signstfvn  32448  signstfvneq0  32451  signsvfn  32461  ivthALT  34451  icorempo  35449  icoreunrn  35457  iooelexlt  35460  relowlssretop  35461  relowlpssretop  35462  poimir  35737  mblfinlem2  35742  iblabsnclem  35767  ftc1anclem1  35777  ftc1anclem6  35782  areacirclem5  35796  areacirc  35797  blbnd  35872  iocmbl  40960  reabssgn  41133  supxrre3  42754  supxrgere  42762  infrpge  42780  infxrunb2  42797  infxrbnd2  42798  infleinflem2  42800  xrralrecnnle  42812  supxrunb3  42829  supminfxr2  42899  xrpnf  42916  ioomidp  42942  limsupre  43072  limsupub  43135  limsuppnflem  43141  limsupre3lem  43163  liminfgord  43185  liminflelimsuplem  43206  limsupgtlem  43208  limsupub2  43243  xlimpnfxnegmnf  43245  xlimmnfvlem2  43264  xlimmnfv  43265  xlimpnfvlem2  43268  xlimpnfv  43269  icccncfext  43318  volioc  43403  volico  43414  fourierdlem113  43650  meaiuninclem  43908  meaiuninc3v  43912  icoresmbl  43971  ovolval5lem1  44080  mbfresmf  44162  cnfsmf  44163  incsmf  44165  smfconst  44172  decsmf  44189  smfres  44211  smfco  44223  issmfle2d  44229  bgoldbtbndlem3  45147  rrxsphere  45982  i0oii  46101  io1ii  46102