Theorem rexrd 7969

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 7773  ℝ^*cxr 7953

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-xr 7958

This theorem is referenced by:  xnn0xr  9203  rpxr  9618  rpxrd  9654  xnn0dcle  9759  xnegcl  9789  xaddf  9801  xaddval  9802  xnn0lenn0nn0  9822  xposdif  9839  iooshf  9909  icoshftf1o  9948  ioo0  10216  ioom  10217  ico0  10218  ioc0  10219  modqelico  10290  mulqaddmodid  10320  addmodid  10328  elicc4abs  11058  xrmaxiflemcl  11208  fprodge1  11602  pcxcl  12265  pcdvdsb  12273  pcaddlem  12292  pcadd  12293  xblss2ps  13198  xblss2  13199  blss2ps  13200  blss2  13201  blhalf  13202  cnblcld  13329  ioo2blex  13338  tgioo  13340  cnopnap  13388  suplociccreex  13396  suplociccex  13397  dedekindicc  13405  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthdec  13416  sin0pilem2  13497  pilem3  13498