Theorem rexr 11122

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 10971  ℝ^*cxr 11109

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-un 3903  df-in 3905  df-ss 3915  df-xr 11114

This theorem is referenced by:  rexri  11134  lenlt  11154  ltpnf  12957  mnflt  12960  xrltnsym  12972  xrlttr  12975  xrre  13004  xrre3  13006  max1  13020  max2  13022  min1  13024  min2  13025  maxle  13026  lemin  13027  maxlt  13028  ltmin  13029  max0sub  13031  qbtwnxr  13035  xralrple  13040  alrple  13041  xltnegi  13051  rexadd  13067  xaddnemnf  13071  xaddnepnf  13072  xaddcom  13075  xnegdi  13083  xpncan  13086  xnpcan  13087  xleadd1a  13088  xleadd1  13090  xltadd1  13091  xltadd2  13092  xsubge0  13096  rexmul  13106  xadddilem  13129  xadddir  13131  xrsupsslem  13142  xrinfmsslem  13143  xrub  13147  supxrun  13151  supxrunb1  13154  supxrunb2  13155  supxrbnd1  13156  supxrbnd2  13157  xrsup0  13158  supxrbnd  13163  infmremnf  13178  elioo4g  13240  elioc2  13243  elico2  13244  elicc2  13245  iccss  13248  iooshf  13259  iooneg  13304  icoshft  13306  difreicc  13317  hashbnd  14151  elicc4abs  15130  icodiamlt  15246  limsupgord  15280  pcadd  16687  ramubcl  16816  lt6abl  19591  xrsmcmn  20727  xrs1mnd  20742  xrs10  20743  xrsdsreval  20749  psmetge0  23571  xmetge0  23603  imasdsf1olem  23632  bl2in  23659  blssps  23683  blss  23684  blcld  23767  icopnfcld  24037  iocmnfcld  24038  bl2ioo  24061  blssioo  24064  xrtgioo  24075  xrsblre  24080  iccntr  24090  icccmplem2  24092  icccmp  24094  reconnlem2  24096  xrge0tsms  24103  icoopnst  24208  iocopnst  24209  ovolfioo  24737  ovolicc2lem1  24787  ovolicc2lem5  24791  voliunlem3  24822  icombl1  24833  icombl  24834  iccvolcl  24837  ovolioo  24838  ioovolcl  24840  uniiccdif  24848  volsup2  24875  mbfimasn  24902  ismbf3d  24924  mbfsup  24934  itg2seq  25013  bddiblnc  25112  dvlip2  25265  ply1remlem  25433  abelthlem3  25698  abelth  25706  sincosq2sgn  25762  sincosq3sgn  25763  sinq12ge0  25771  sincos6thpi  25778  sineq0  25786  efif1olem1  25804  efif1olem2  25805  efif1o  25808  eff1o  25811  loglesqrt  26017  basellem1  26336  pntlemo  26861  nmobndi  29425  nmopub2tALT  30559  nmfnleub2  30576  nmopcoadji  30751  rexdiv  31487  xrge0tsmsd  31604  pnfneige0  32199  lmxrge0  32200  hashf2  32350  sxbrsigalem0  32538  orvcgteel  32734  orvclteel  32739  sgnclre  32806  sgnneg  32807  signstfvn  32848  signstfvneq0  32851  signsvfn  32861  ivthALT  34620  icorempo  35635  icoreunrn  35643  iooelexlt  35646  relowlssretop  35647  relowlpssretop  35648  poimir  35923  mblfinlem2  35928  iblabsnclem  35953  ftc1anclem1  35963  ftc1anclem6  35968  areacirclem5  35982  areacirc  35983  blbnd  36058  iocmbl  41316  reabssgn  41574  supxrre3  43208  supxrgere  43216  infrpge  43234  infxrunb2  43251  infxrbnd2  43252  infleinflem2  43254  xrralrecnnle  43266  supxrunb3  43283  supminfxr2  43353  xrpnf  43370  ioomidp  43397  limsupre  43527  limsupub  43590  limsuppnflem  43596  limsupre3lem  43618  liminfgord  43640  liminflelimsuplem  43661  limsupgtlem  43663  limsupub2  43698  xlimpnfxnegmnf  43700  xlimmnfvlem2  43719  xlimmnfv  43720  xlimpnfvlem2  43723  xlimpnfv  43724  icccncfext  43773  volioc  43858  volico  43869  fourierdlem113  44105  meaiuninclem  44364  meaiuninc3v  44368  icoresmbl  44427  ovolval5lem1  44536  mbfresmf  44623  cnfsmf  44624  incsmf  44626  smfconst  44633  decsmf  44651  smfres  44674  smfco  44686  issmfle2d  44693  bgoldbtbndlem3  45619  rrxsphere  46454  i0oii  46573  io1ii  46574