Theorem rexr 11273

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℝ^*cxr 11260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-xr 11265

This theorem is used by:  rexri  11285  lenlt  11306  ltpnf  13163  mnflt  13166  xrltnsym  13180  xrlttr  13183  xrre  13213  xrre3  13215  max1  13229  max2  13231  min1  13233  min2  13234  maxle  13235  lemin  13236  maxlt  13237  ltmin  13238  max0sub  13240  qbtwnxr  13244  xralrple  13249  alrple  13250  xltnegi  13260  rexadd  13276  xaddnemnf  13280  xaddnepnf  13281  xaddcom  13284  xnegdi  13292  xpncan  13295  xnpcan  13296  xleadd1a  13297  xleadd1  13299  xltadd1  13300  xltadd2  13301  xsubge0  13305  rexmul  13315  xadddilem  13338  xadddir  13340  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  supxrun  13360  supxrunb1  13363  supxrunb2  13364  supxrbnd1  13365  supxrbnd2  13366  xrsup0  13367  supxrbnd  13372  infmremnf  13388  elioo4g  13451  elioc2  13454  elico2  13455  elicc2  13456  iccss  13459  iooshf  13471  iooneg  13516  icoshft  13518  difreicc  13529  hashbnd  14392  sgnneg  15163  sgnclre  15165  elicc4abs  15397  icodiamlt  15515  limsupgord  15549  pcadd  16974  ramubcl  17103  lt6abl  19996  xrsmcmn  21582  xrsdsreval  21599  xrs1mnd  21627  xrs10  21628  psmetge0  24506  xmetge0  24538  imasdsf1olem  24567  bl2in  24594  blssps  24618  blss  24619  blcld  24699  icopnfcld  24961  iocmnfcld  24962  bl2ioo  24986  blssioo  24989  xrtgioo  25001  xrsblre  25006  iccntr  25016  icccmplem2  25018  icccmp  25020  reconnlem2  25022  xrge0tsms  25029  icoopnst  25135  iocopnst  25136  ovolfioo  25663  ovolicc2lem1  25713  ovolicc2lem5  25717  voliunlem3  25748  icombl1  25759  icombl  25760  iccvolcl  25763  ovolioo  25764  ioovolcl  25766  uniiccdif  25774  volsup2  25801  mbfimasn  25828  ismbf3d  25850  mbfsup  25860  itg2seq  25938  bddiblnc  26038  dvlip2  26191  ply1remlem  26359  abelthlem3  26633  abelth  26641  sincosq2sgn  26701  sincosq3sgn  26702  sinq12ge0  26710  sincos6thpi  26718  sineq0  26726  efif1olem1  26744  efif1olem2  26745  efif1o  26748  eff1o  26751  loglesqrt  26963  basellem1  27282  pntlemo  27808  nmobndi  31164  nmopub2tALT  32298  nmfnleub2  32315  nmopcoadji  32490  rexdiv  33282  xrge0tsmsd  33424  pnfneige0  34372  lmxrge0  34373  hashf2  34505  sxbrsigalem0  34693  orvcgteel  34890  orvclteel  34895  signstfvn  34988  signstfvneq0  34991  signsvfn  35001  ivthALT  36887  icorempo  38038  icoreunrn  38046  iooelexlt  38049  relowlssretop  38050  relowlpssretop  38051  poimir  38345  mblfinlem2  38350  iblabsnclem  38375  ftc1anclem1  38385  ftc1anclem6  38390  areacirclem5  38404  areacirc  38405  blbnd  38479  iocmbl  43981  reabssgn  44403  supxrre3  46082  supxrgere  46090  infrpge  46108  infxrunb2  46124  infxrbnd2  46125  infleinflem2  46127  xrralrecnnle  46139  supxrunb3  46155  supminfxr2  46224  xrpnf  46240  ioomidp  46271  limsupre  46396  limsupub  46459  limsuppnflem  46465  limsupre3lem  46487  liminfgord  46509  liminflelimsuplem  46530  limsupgtlem  46532  limsupub2  46567  xlimpnfxnegmnf  46569  xlimmnfvlem2  46588  xlimmnfv  46589  xlimpnfvlem2  46592  xlimpnfv  46593  icccncfext  46642  volioc  46727  volico  46738  fourierdlem113  46974  meaiuninclem  47235  meaiuninc3v  47239  icoresmbl  47298  ovolval5lem1  47407  mbfresmf  47494  cnfsmf  47495  incsmf  47497  smfconst  47504  decsmf  47522  smfres  47545  smfco  47557  issmfle2d  47564  finfdm  47601  bgoldbtbndlem3  48613  rrxsphere  49569  i0oii  49739  io1ii  49740