Theorem rexrd 8229

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℝ^*cxr 8213

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-xr 8218

This theorem is referenced by:  xnn0xr  9470  rpxr  9896  rpxrd  9932  xnn0dcle  10037  xnegcl  10067  xaddf  10079  xaddval  10080  xnn0lenn0nn0  10100  xposdif  10117  iooshf  10187  icoshftf1o  10226  ioo0  10520  ioom  10521  ico0  10522  ioc0  10523  xqltnle  10528  modqelico  10597  mulqaddmodid  10627  addmodid  10635  elicc4abs  11659  xrmaxiflemcl  11810  fprodge1  12205  pcxcl  12889  pcdvdsb  12898  pcaddlem  12917  pcadd  12918  xblss2ps  15134  xblss2  15135  blss2ps  15136  blss2  15137  blhalf  15138  cnblcld  15265  ioo2blex  15282  tgioo  15284  cnopnap  15341  suplociccreex  15354  suplociccex  15355  dedekindicc  15363  ivthinclemlm  15364  ivthinclemum  15365  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthdec  15374  ivthreinc  15375  sin0pilem2  15512  pilem3  15513  vtxdgfifival  16148