Theorem rexr 11178

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℝ^*cxr 11165

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170

This theorem is referenced by:  rexri  11190  lenlt  11211  ltpnf  13034  mnflt  13037  xrltnsym  13051  xrlttr  13054  xrre  13084  xrre3  13086  max1  13100  max2  13102  min1  13104  min2  13105  maxle  13106  lemin  13107  maxlt  13108  ltmin  13109  max0sub  13111  qbtwnxr  13115  xralrple  13120  alrple  13121  xltnegi  13131  rexadd  13147  xaddnemnf  13151  xaddnepnf  13152  xaddcom  13155  xnegdi  13163  xpncan  13166  xnpcan  13167  xleadd1a  13168  xleadd1  13170  xltadd1  13171  xltadd2  13172  xsubge0  13176  rexmul  13186  xadddilem  13209  xadddir  13211  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxrun  13231  supxrunb1  13234  supxrunb2  13235  supxrbnd1  13236  supxrbnd2  13237  xrsup0  13238  supxrbnd  13243  infmremnf  13259  elioo4g  13322  elioc2  13325  elico2  13326  elicc2  13327  iccss  13330  iooshf  13342  iooneg  13387  icoshft  13389  difreicc  13400  hashbnd  14259  elicc4abs  15243  icodiamlt  15361  limsupgord  15395  pcadd  16817  ramubcl  16946  lt6abl  19824  xrsmcmn  21346  xrsdsreval  21366  xrs1mnd  21395  xrs10  21396  psmetge0  24256  xmetge0  24288  imasdsf1olem  24317  bl2in  24344  blssps  24368  blss  24369  blcld  24449  icopnfcld  24711  iocmnfcld  24712  bl2ioo  24736  blssioo  24739  xrtgioo  24751  xrsblre  24756  iccntr  24766  icccmplem2  24768  icccmp  24770  reconnlem2  24772  xrge0tsms  24779  icoopnst  24892  iocopnst  24893  ovolfioo  25424  ovolicc2lem1  25474  ovolicc2lem5  25478  voliunlem3  25509  icombl1  25520  icombl  25521  iccvolcl  25524  ovolioo  25525  ioovolcl  25527  uniiccdif  25535  volsup2  25562  mbfimasn  25589  ismbf3d  25611  mbfsup  25621  itg2seq  25699  bddiblnc  25799  dvlip2  25956  ply1remlem  26126  abelthlem3  26399  abelth  26407  sincosq2sgn  26464  sincosq3sgn  26465  sinq12ge0  26473  sincos6thpi  26481  sineq0  26489  efif1olem1  26507  efif1olem2  26508  efif1o  26511  eff1o  26514  loglesqrt  26727  basellem1  27047  pntlemo  27574  nmobndi  30850  nmopub2tALT  31984  nmfnleub2  32001  nmopcoadji  32176  sgnclre  32913  sgnneg  32914  rexdiv  33007  xrge0tsmsd  33155  pnfneige0  34108  lmxrge0  34109  hashf2  34241  sxbrsigalem0  34428  orvcgteel  34625  orvclteel  34630  signstfvn  34726  signstfvneq0  34729  signsvfn  34739  ivthALT  36529  icorempo  37552  icoreunrn  37560  iooelexlt  37563  relowlssretop  37564  relowlpssretop  37565  poimir  37850  mblfinlem2  37855  iblabsnclem  37880  ftc1anclem1  37890  ftc1anclem6  37895  areacirclem5  37909  areacirc  37910  blbnd  37984  iocmbl  43451  reabssgn  43873  supxrre3  45566  supxrgere  45574  infrpge  45592  infxrunb2  45608  infxrbnd2  45609  infleinflem2  45611  xrralrecnnle  45623  supxrunb3  45639  supminfxr2  45709  xrpnf  45725  ioomidp  45756  limsupre  45881  limsupub  45944  limsuppnflem  45950  limsupre3lem  45972  liminfgord  45994  liminflelimsuplem  46015  limsupgtlem  46017  limsupub2  46052  xlimpnfxnegmnf  46054  xlimmnfvlem2  46073  xlimmnfv  46074  xlimpnfvlem2  46077  xlimpnfv  46078  icccncfext  46127  volioc  46212  volico  46223  fourierdlem113  46459  meaiuninclem  46720  meaiuninc3v  46724  icoresmbl  46783  ovolval5lem1  46892  mbfresmf  46979  cnfsmf  46980  incsmf  46982  smfconst  46989  decsmf  47007  smfres  47030  smfco  47042  issmfle2d  47049  finfdm  47086  bgoldbtbndlem3  48049  rrxsphere  48990  i0oii  49161  io1ii  49162