Theorem rexr 7683

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

Syntax hints:   → wi 4   ∈ wcel 1448  ℝcr 7499  ℝ^*cxr 7671

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-xr 7676

This theorem is referenced by:  rexri  7695  lenlt  7711  ltpnf  9408  mnflt  9410  xrltnsym  9420  xrlttr  9422  xrltso  9423  xrre  9444  xrre3  9446  xltnegi  9459  rexadd  9476  xaddnemnf  9481  xaddnepnf  9482  xaddcom  9485  xnegdi  9492  xpncan  9495  xnpcan  9496  xleadd1a  9497  xleadd1  9499  xltadd1  9500  xltadd2  9501  xsubge0  9505  xposdif  9506  elioo4g  9558  elioc2  9560  elico2  9561  elicc2  9562  iccss  9565  iooshf  9576  iooneg  9612  icoshft  9614  qbtwnxr  9876  modqmuladdim  9981  elicc4abs  10706  icodiamlt  10792  xrmaxrecl  10863  xrmaxaddlem  10868  xrminrecl  10881  bl2in  12331  blssps  12355  blss  12356  bl2ioo  12461  blssioo  12464