Theorem rexr 10533

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

Syntax hints:   → wi 4   ∈ wcel 2081  ℝcr 10382  ℝ^*cxr 10520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-un 3864  df-in 3866  df-ss 3874  df-xr 10525

This theorem is referenced by:  rexri  10546  lenlt  10566  ltpnf  12365  mnflt  12368  xrltnsym  12380  xrlttr  12383  xrre  12412  xrre3  12414  max1  12428  max2  12430  min1  12432  min2  12433  maxle  12434  lemin  12435  maxlt  12436  ltmin  12437  max0sub  12439  qbtwnxr  12443  xralrple  12448  alrple  12449  xltnegi  12459  rexadd  12475  xaddnemnf  12479  xaddnepnf  12480  xaddcom  12483  xnegdi  12491  xpncan  12494  xnpcan  12495  xleadd1a  12496  xleadd1  12498  xltadd1  12499  xltadd2  12500  xsubge0  12504  rexmul  12514  xadddilem  12537  xadddir  12539  xrsupsslem  12550  xrinfmsslem  12551  xrub  12555  supxrun  12559  supxrunb1  12562  supxrunb2  12563  supxrbnd1  12564  supxrbnd2  12565  xrsup0  12566  supxrbnd  12571  infmremnf  12586  elioo4g  12647  elioc2  12649  elico2  12650  elicc2  12651  iccss  12654  iooshf  12665  iooneg  12707  icoshft  12709  difreicc  12720  hashbnd  13546  elicc4abs  14513  icodiamlt  14629  limsupgord  14663  pcadd  16054  ramubcl  16183  lt6abl  18736  xrsmcmn  20250  xrs1mnd  20265  xrs10  20266  xrsdsreval  20272  psmetge0  22605  xmetge0  22637  imasdsf1olem  22666  bl2in  22693  blssps  22717  blss  22718  blcld  22798  icopnfcld  23059  iocmnfcld  23060  bl2ioo  23083  blssioo  23086  xrtgioo  23097  xrsblre  23102  iccntr  23112  icccmplem2  23114  icccmp  23116  reconnlem2  23118  xrge0tsms  23125  icoopnst  23226  iocopnst  23227  ovolfioo  23751  ovolicc2lem1  23801  ovolicc2lem5  23805  voliunlem3  23836  icombl1  23847  icombl  23848  iccvolcl  23851  ovolioo  23852  ioovolcl  23854  uniiccdif  23862  volsup2  23889  mbfimasn  23916  ismbf3d  23938  mbfsup  23948  itg2seq  24026  dvlip2  24275  ply1remlem  24439  abelthlem3  24704  abelth  24712  sincosq2sgn  24768  sincosq3sgn  24769  sinq12ge0  24777  sincos6thpi  24784  sineq0  24792  efif1olem1  24807  efif1olem2  24808  efif1o  24811  eff1o  24814  loglesqrt  25020  basellem1  25340  pntlemo  25865  nmobndi  28243  nmopub2tALT  29377  nmfnleub2  29394  nmopcoadji  29569  rexdiv  30286  xrge0tsmsd  30503  pnfneige0  30811  lmxrge0  30812  hashf2  30960  sxbrsigalem0  31146  orvcgteel  31342  orvclteel  31347  sgnclre  31414  sgnneg  31415  signstfvneq0  31459  ivthALT  33292  icorempo  34163  icoreunrn  34171  iooelexlt  34174  relowlssretop  34175  relowlpssretop  34176  poimir  34456  mblfinlem2  34461  iblabsnclem  34486  bddiblnc  34493  ftc1anclem1  34498  ftc1anclem6  34503  areacirclem5  34517  areacirc  34518  blbnd  34597  iocmbl  39304  supxrre3  41134  supxrgere  41142  infrpge  41160  infxrunb2  41177  infxrbnd2  41178  infleinflem2  41180  xrralrecnnle  41194  supxrunb3  41213  supminfxr2  41287  xrpnf  41304  ioomidp  41332  limsupre  41464  limsupub  41527  limsuppnflem  41533  limsupre3lem  41555  liminfgord  41577  liminflelimsuplem  41598  limsupgtlem  41600  limsupub2  41635  xlimpnfxnegmnf  41637  xlimmnfvlem2  41656  xlimmnfv  41657  xlimpnfvlem2  41660  xlimpnfv  41661  icccncfext  41711  volioc  41798  volico  41810  fourierdlem113  42046  meaiuninclem  42304  meaiuninc3v  42308  icoresmbl  42367  ovolval5lem1  42476  mbfresmf  42558  cnfsmf  42559  incsmf  42561  smfconst  42568  decsmf  42585  smfres  42607  smfco  42619  issmfle2d  42625  bgoldbtbndlem3  43454  rrxsphere  44216