Theorem rexr 8160

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℝcr 7966  ℝ^*cxr 8148

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-xr 8153

This theorem is referenced by:  rexri  8172  lenlt  8190  ltpnf  9944  mnflt  9947  xrltnsym  9957  xrlttr  9959  xrltso  9960  xrre  9984  xrre3  9986  xltnegi  9999  rexadd  10016  xaddnemnf  10021  xaddnepnf  10022  xaddcom  10025  xnegdi  10032  xpncan  10035  xnpcan  10036  xleadd1a  10037  xleadd1  10039  xltadd1  10040  xltadd2  10041  xsubge0  10045  xposdif  10046  elioo4g  10098  elioc2  10100  elico2  10101  elicc2  10102  iccss  10105  iooshf  10116  iooneg  10152  icoshft  10154  qbtwnxr  10444  modqmuladdim  10556  elicc4abs  11571  icodiamlt  11657  xrmaxrecl  11732  xrmaxaddlem  11737  xrminrecl  11750  bl2in  15042  blssps  15066  blss  15067  reopnap  15185  bl2ioo  15189  blssioo  15192  sincosq2sgn  15466  sincosq3sgn  15467  sincos6thpi  15481