Theorem rexr 11225

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921  df-xr 11217

This theorem is referenced by:  rexri  11237  lenlt  11258  ltpnf  13119  mnflt  13122  xrltnsym  13136  xrlttr  13139  xrre  13169  xrre3  13171  max1  13185  max2  13187  min1  13189  min2  13190  maxle  13191  lemin  13192  maxlt  13193  ltmin  13194  max0sub  13196  qbtwnxr  13200  xralrple  13205  alrple  13206  xltnegi  13216  rexadd  13232  xaddnemnf  13236  xaddnepnf  13237  xaddcom  13240  xnegdi  13248  xpncan  13251  xnpcan  13252  xleadd1a  13253  xleadd1  13255  xltadd1  13256  xltadd2  13257  xsubge0  13261  rexmul  13271  xadddilem  13294  xadddir  13296  xrsupsslem  13307  xrinfmsslem  13308  xrub  13312  supxrun  13316  supxrunb1  13319  supxrunb2  13320  supxrbnd1  13321  supxrbnd2  13322  xrsup0  13323  supxrbnd  13328  infmremnf  13344  elioo4g  13407  elioc2  13410  elico2  13411  elicc2  13412  iccss  13415  iooshf  13427  iooneg  13472  icoshft  13474  difreicc  13485  hashbnd  14346  elicc4abs  15330  icodiamlt  15448  limsupgord  15482  pcadd  16908  ramubcl  17037  lt6abl  19918  xrsmcmn  21427  xrsdsreval  21444  xrs1mnd  21472  xrs10  21473  psmetge0  24352  xmetge0  24384  imasdsf1olem  24413  bl2in  24440  blssps  24464  blss  24465  blcld  24545  icopnfcld  24807  iocmnfcld  24808  bl2ioo  24832  blssioo  24835  xrtgioo  24847  xrsblre  24852  iccntr  24862  icccmplem2  24864  icccmp  24866  reconnlem2  24868  xrge0tsms  24875  icoopnst  24981  iocopnst  24982  ovolfioo  25509  ovolicc2lem1  25559  ovolicc2lem5  25563  voliunlem3  25594  icombl1  25605  icombl  25606  iccvolcl  25609  ovolioo  25610  ioovolcl  25612  uniiccdif  25620  volsup2  25647  mbfimasn  25674  ismbf3d  25696  mbfsup  25706  itg2seq  25784  bddiblnc  25884  dvlip2  26037  ply1remlem  26205  abelthlem3  26473  abelth  26481  sincosq2sgn  26541  sincosq3sgn  26542  sinq12ge0  26550  sincos6thpi  26558  sineq0  26566  efif1olem1  26584  efif1olem2  26585  efif1o  26588  eff1o  26591  loglesqrt  26803  basellem1  27122  pntlemo  27648  nmobndi  30924  nmopub2tALT  32058  nmfnleub2  32075  nmopcoadji  32250  sgnclre  32984  sgnneg  32985  rexdiv  33064  xrge0tsmsd  33214  pnfneige0  34209  lmxrge0  34210  hashf2  34342  sxbrsigalem0  34529  orvcgteel  34726  orvclteel  34731  signstfvn  34827  signstfvneq0  34830  signsvfn  34840  ivthALT  36659  icorempo  37809  icoreunrn  37817  iooelexlt  37820  relowlssretop  37821  relowlpssretop  37822  poimir  38116  mblfinlem2  38121  iblabsnclem  38146  ftc1anclem1  38156  ftc1anclem6  38161  areacirclem5  38175  areacirc  38176  blbnd  38250  iocmbl  43754  reabssgn  44176  supxrre3  45865  supxrgere  45873  infrpge  45891  infxrunb2  45907  infxrbnd2  45908  infleinflem2  45910  xrralrecnnle  45922  supxrunb3  45938  supminfxr2  46007  xrpnf  46023  ioomidp  46054  limsupre  46179  limsupub  46242  limsuppnflem  46248  limsupre3lem  46270  liminfgord  46292  liminflelimsuplem  46313  limsupgtlem  46315  limsupub2  46350  xlimpnfxnegmnf  46352  xlimmnfvlem2  46371  xlimmnfv  46372  xlimpnfvlem2  46375  xlimpnfv  46376  icccncfext  46425  volioc  46510  volico  46521  fourierdlem113  46757  meaiuninclem  47018  meaiuninc3v  47022  icoresmbl  47081  ovolval5lem1  47190  mbfresmf  47277  cnfsmf  47278  incsmf  47280  smfconst  47287  decsmf  47305  smfres  47328  smfco  47340  issmfle2d  47347  finfdm  47384  bgoldbtbndlem3  48393  rrxsphere  49334  i0oii  49505  io1ii  49506