Theorem rexr 8315

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8122  ℝ^*cxr 8303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-xr 8308

This theorem is referenced by:  rexri  8327  lenlt  8345  ltpnf  10109  mnflt  10112  xrltnsym  10122  xrlttr  10124  xrltso  10125  xrre  10149  xrre3  10151  xltnegi  10164  rexadd  10181  xaddnemnf  10186  xaddnepnf  10187  xaddcom  10190  xnegdi  10197  xpncan  10200  xnpcan  10201  xleadd1a  10202  xleadd1  10204  xltadd1  10205  xltadd2  10206  xsubge0  10210  xposdif  10211  elioo4g  10263  elioc2  10265  elico2  10266  elicc2  10267  iccss  10270  iooshf  10281  iooneg  10317  icoshft  10319  qbtwnxr  10613  modqmuladdim  10725  elicc4abs  11772  icodiamlt  11858  xrmaxrecl  11933  xrmaxaddlem  11938  xrminrecl  11951  bl2in  15255  blssps  15279  blss  15280  reopnap  15398  bl2ioo  15402  blssioo  15405  sincosq2sgn  15679  sincosq3sgn  15680  sincos6thpi  15694