Theorem rexr 8230

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℝcr 8036  ℝ^*cxr 8218

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-xr 8223

This theorem is referenced by:  rexri  8242  lenlt  8260  ltpnf  10020  mnflt  10023  xrltnsym  10033  xrlttr  10035  xrltso  10036  xrre  10060  xrre3  10062  xltnegi  10075  rexadd  10092  xaddnemnf  10097  xaddnepnf  10098  xaddcom  10101  xnegdi  10108  xpncan  10111  xnpcan  10112  xleadd1a  10113  xleadd1  10115  xltadd1  10116  xltadd2  10117  xsubge0  10121  xposdif  10122  elioo4g  10174  elioc2  10176  elico2  10177  elicc2  10178  iccss  10181  iooshf  10192  iooneg  10228  icoshft  10230  qbtwnxr  10523  modqmuladdim  10635  elicc4abs  11677  icodiamlt  11763  xrmaxrecl  11838  xrmaxaddlem  11843  xrminrecl  11856  bl2in  15156  blssps  15180  blss  15181  reopnap  15299  bl2ioo  15303  blssioo  15306  sincosq2sgn  15580  sincosq3sgn  15581  sincos6thpi  15595