Theorem rexr 8072

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7878  ℝ^*cxr 8060

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-xr 8065

This theorem is referenced by:  rexri  8084  lenlt  8102  ltpnf  9855  mnflt  9858  xrltnsym  9868  xrlttr  9870  xrltso  9871  xrre  9895  xrre3  9897  xltnegi  9910  rexadd  9927  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xnegdi  9943  xpncan  9946  xnpcan  9947  xleadd1a  9948  xleadd1  9950  xltadd1  9951  xltadd2  9952  xsubge0  9956  xposdif  9957  elioo4g  10009  elioc2  10011  elico2  10012  elicc2  10013  iccss  10016  iooshf  10027  iooneg  10063  icoshft  10065  qbtwnxr  10347  modqmuladdim  10459  elicc4abs  11259  icodiamlt  11345  xrmaxrecl  11420  xrmaxaddlem  11425  xrminrecl  11438  bl2in  14639  blssps  14663  blss  14664  reopnap  14782  bl2ioo  14786  blssioo  14789  sincosq2sgn  15063  sincosq3sgn  15064  sincos6thpi  15078