Theorem rexrd 8006

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7809  ℝ^*cxr 7990

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-xr 7995

This theorem is referenced by:  xnn0xr  9243  rpxr  9660  rpxrd  9696  xnn0dcle  9801  xnegcl  9831  xaddf  9843  xaddval  9844  xnn0lenn0nn0  9864  xposdif  9881  iooshf  9951  icoshftf1o  9990  ioo0  10259  ioom  10260  ico0  10261  ioc0  10262  modqelico  10333  mulqaddmodid  10363  addmodid  10371  elicc4abs  11102  xrmaxiflemcl  11252  fprodge1  11646  pcxcl  12310  pcdvdsb  12318  pcaddlem  12337  pcadd  12338  xblss2ps  13874  xblss2  13875  blss2ps  13876  blss2  13877  blhalf  13878  cnblcld  14005  ioo2blex  14014  tgioo  14016  cnopnap  14064  suplociccreex  14072  suplociccex  14073  dedekindicc  14081  ivthinclemlm  14082  ivthinclemum  14083  ivthinclemlopn  14084  ivthinclemuopn  14086  ivthdec  14092  sin0pilem2  14173  pilem3  14174