Theorem rexr 8218

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  ℝ^*cxr 8206

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-xr 8211

This theorem is referenced by:  rexri  8230  lenlt  8248  ltpnf  10008  mnflt  10011  xrltnsym  10021  xrlttr  10023  xrltso  10024  xrre  10048  xrre3  10050  xltnegi  10063  rexadd  10080  xaddnemnf  10085  xaddnepnf  10086  xaddcom  10089  xnegdi  10096  xpncan  10099  xnpcan  10100  xleadd1a  10101  xleadd1  10103  xltadd1  10104  xltadd2  10105  xsubge0  10109  xposdif  10110  elioo4g  10162  elioc2  10164  elico2  10165  elicc2  10166  iccss  10169  iooshf  10180  iooneg  10216  icoshft  10218  qbtwnxr  10510  modqmuladdim  10622  elicc4abs  11648  icodiamlt  11734  xrmaxrecl  11809  xrmaxaddlem  11814  xrminrecl  11827  bl2in  15120  blssps  15144  blss  15145  reopnap  15263  bl2ioo  15267  blssioo  15270  sincosq2sgn  15544  sincosq3sgn  15545  sincos6thpi  15559