Theorem rexr 11358

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-xr 11350

This theorem is used by:  rexri  11370  lenlt  11391  ltpnf  13252  mnflt  13255  xrltnsym  13269  xrlttr  13272  xrre  13302  xrre3  13304  max1  13318  max2  13320  min1  13322  min2  13323  maxle  13324  lemin  13325  maxlt  13326  ltmin  13327  max0sub  13329  qbtwnxr  13333  xralrple  13338  alrple  13339  xltnegi  13349  rexadd  13365  xaddnemnf  13369  xaddnepnf  13370  xaddcom  13373  xnegdi  13381  xpncan  13384  xnpcan  13385  xleadd1a  13386  xleadd1  13388  xltadd1  13389  xltadd2  13390  xsubge0  13394  rexmul  13404  xadddilem  13427  xadddir  13429  xrsupsslem  13440  xrinfmsslem  13441  xrub  13445  supxrun  13449  supxrunb1  13452  supxrunb2  13453  supxrbnd1  13454  supxrbnd2  13455  xrsup0  13456  supxrbnd  13461  infmremnf  13477  elioo4g  13540  elioc2  13543  elico2  13544  elicc2  13545  iccss  13548  iooshf  13560  iooneg  13605  icoshft  13607  difreicc  13618  hashbnd  14483  sgnneg  15258  sgnclre  15260  elicc4abs  15492  icodiamlt  15610  limsupgord  15644  pcadd  17072  ramubcl  17201  lt6abl  20114  xrsmcmn  21706  xrsdsreval  21723  xrs1mnd  21751  xrs10  21752  psmetge0  24636  xmetge0  24668  imasdsf1olem  24697  bl2in  24724  blssps  24748  blss  24749  blcld  24829  icopnfcld  25091  iocmnfcld  25092  bl2ioo  25116  blssioo  25119  xrtgioo  25131  xrsblre  25136  iccntr  25146  icccmplem2  25148  icccmp  25150  reconnlem2  25152  xrge0tsms  25159  icoopnst  25265  iocopnst  25266  ovolfioo  25793  ovolicc2lem1  25843  ovolicc2lem5  25847  voliunlem3  25878  icombl1  25889  icombl  25890  iccvolcl  25893  ovolioo  25894  ioovolcl  25896  uniiccdif  25904  volsup2  25931  mbfimasn  25958  ismbf3d  25980  mbfsup  25990  itg2seq  26068  bddiblnc  26167  dvlip2  26320  ply1remlem  26488  abelthlem3  26765  abelth  26773  sincosq2sgn  26833  sincosq3sgn  26834  sinq12ge0  26842  sincos6thpi  26849  sineq0  26857  efif1olem1  26875  efif1olem2  26876  efif1o  26879  eff1o  26882  loglesqrt  27094  basellem1  27413  pntlemo  27939  nmobndi  31382  nmopub2tALT  32516  nmfnleub2  32533  nmopcoadji  32708  rexdiv  33538  xrge0tsmsd  33680  pnfneige0  34629  lmxrge0  34630  hashf2  34762  sxbrsigalem0  34949  orvcgteel  35146  orvclteel  35151  signstfvn  35244  signstfvneq0  35247  signsvfn  35257  ivthALT  37215  icorempo  38367  icoreunrn  38375  iooelexlt  38378  relowlssretop  38379  relowlpssretop  38380  poimir  38664  mblfinlem2  38669  iblabsnclem  38694  ftc1anclem1  38704  ftc1anclem6  38709  areacirclem5  38723  areacirc  38724  blbnd  38814  iocmbl  44308  reabssgn  44729  supxrre3  46430  supxrgere  46438  infrpge  46456  infxrunb2  46472  infxrbnd2  46473  infleinflem2  46475  xrralrecnnle  46487  supxrunb3  46503  supminfxr2  46572  xrpnf  46588  ioomidp  46619  limsupre  46744  limsupub  46807  limsuppnflem  46813  limsupre3lem  46835  liminfgord  46857  liminflelimsuplem  46878  limsupgtlem  46880  limsupub2  46915  xlimpnfxnegmnf  46917  xlimmnfvlem2  46936  xlimmnfv  46937  xlimpnfvlem2  46940  xlimpnfv  46941  icccncfext  46990  volioc  47075  volico  47086  fourierdlem113  47322  meaiuninclem  47583  meaiuninc3v  47587  icoresmbl  47646  ovolval5lem1  47755  mbfresmf  47842  cnfsmf  47843  incsmf  47845  smfconst  47852  decsmf  47870  smfres  47893  smfco  47905  issmfle2d  47912  finfdm  47949  bgoldbtbndlem3  48998  rrxsphere  49953  i0oii  50127  io1ii  50128