Theorem rexrd 7839

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 7833	. 2 ⊢ ℝ ⊆ ℝ*
2		rexrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	1, 2	sseldi 3100	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  ℝ^*cxr 7823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-xr 7828

This theorem is referenced by:  xnn0xr  9069  rpxr  9478  rpxrd  9514  xnegcl  9645  xaddf  9657  xaddval  9658  xnn0lenn0nn0  9678  xposdif  9695  iooshf  9765  icoshftf1o  9804  ioo0  10068  ioom  10069  ico0  10070  ioc0  10071  modqelico  10138  mulqaddmodid  10168  addmodid  10176  elicc4abs  10898  xrmaxiflemcl  11046  xblss2ps  12612  xblss2  12613  blss2ps  12614  blss2  12615  blhalf  12616  cnblcld  12743  ioo2blex  12752  tgioo  12754  cnopnap  12802  suplociccreex  12810  suplociccex  12811  dedekindicc  12819  ivthinclemlm  12820  ivthinclemum  12821  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthdec  12830  sin0pilem2  12911  pilem3  12912