Theorem rexrd 8271

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
rexrd	⊢ (𝜑 → 𝐴 ∈ ℝ*)

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 8265	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sselid 3226	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℝ^*cxr 8255

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-xr 8260

This theorem is referenced by:  xnn0xr  9514  rpxr  9940  rpxrd  9976  xnn0dcle  10081  xnegcl  10111  xaddf  10123  xaddval  10124  xnn0lenn0nn0  10144  xposdif  10161  iooshf  10231  icoshftf1o  10270  ioo0  10565  ioom  10566  ico0  10567  ioc0  10568  xqltnle  10573  modqelico  10642  mulqaddmodid  10672  addmodid  10680  elicc4abs  11717  xrmaxiflemcl  11868  fprodge1  12263  pcxcl  12947  pcdvdsb  12956  pcaddlem  12975  pcadd  12976  xblss2ps  15198  xblss2  15199  blss2ps  15200  blss2  15201  blhalf  15202  cnblcld  15329  ioo2blex  15346  tgioo  15348  cnopnap  15405  suplociccreex  15418  suplociccex  15419  dedekindicc  15427  ivthinclemlm  15428  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthdec  15438  ivthreinc  15439  sin0pilem2  15576  pilem3  15577  vtxdgfifival  16215