Theorem rexrd 8323

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8126  ℝ^*cxr 8307

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-xr 8312

This theorem is referenced by:  xnn0xr  9568  rpxr  9994  rpxrd  10030  xnn0dcle  10135  xnegcl  10165  xaddf  10177  xaddval  10178  xnn0lenn0nn0  10198  xposdif  10215  iooshf  10285  icoshftf1o  10324  ioo0  10619  ioom  10620  ico0  10621  ioc0  10622  xqltnle  10627  modqelico  10696  mulqaddmodid  10726  addmodid  10734  elicc4abs  11779  xrmaxiflemcl  11930  fprodge1  12325  pcxcl  13009  pcdvdsb  13018  pcaddlem  13037  pcadd  13038  xblss2ps  15269  xblss2  15270  blss2ps  15271  blss2  15272  blhalf  15273  cnblcld  15400  ioo2blex  15417  tgioo  15419  cnopnap  15476  suplociccreex  15489  suplociccex  15490  dedekindicc  15498  ivthinclemlm  15499  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthdec  15509  ivthreinc  15510  sin0pilem2  15647  pilem3  15648  vtxdgfifival  16286