Theorem rexrd 8007

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7810  ℝ^*cxr 7991

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 2740  df-un 3134  df-in 3136  df-ss 3143  df-xr 7996

This theorem is referenced by:  xnn0xr  9244  rpxr  9661  rpxrd  9697  xnn0dcle  9802  xnegcl  9832  xaddf  9844  xaddval  9845  xnn0lenn0nn0  9865  xposdif  9882  iooshf  9952  icoshftf1o  9991  ioo0  10260  ioom  10261  ico0  10262  ioc0  10263  modqelico  10334  mulqaddmodid  10364  addmodid  10372  elicc4abs  11103  xrmaxiflemcl  11253  fprodge1  11647  pcxcl  12311  pcdvdsb  12319  pcaddlem  12338  pcadd  12339  xblss2ps  13907  xblss2  13908  blss2ps  13909  blss2  13910  blhalf  13911  cnblcld  14038  ioo2blex  14047  tgioo  14049  cnopnap  14097  suplociccreex  14105  suplociccex  14106  dedekindicc  14114  ivthinclemlm  14115  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthdec  14125  sin0pilem2  14206  pilem3  14207