Theorem rexrd 8212

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℝ^*cxr 8196

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-xr 8201

This theorem is referenced by:  xnn0xr  9453  rpxr  9874  rpxrd  9910  xnn0dcle  10015  xnegcl  10045  xaddf  10057  xaddval  10058  xnn0lenn0nn0  10078  xposdif  10095  iooshf  10165  icoshftf1o  10204  ioo0  10496  ioom  10497  ico0  10498  ioc0  10499  xqltnle  10504  modqelico  10573  mulqaddmodid  10603  addmodid  10611  elicc4abs  11626  xrmaxiflemcl  11777  fprodge1  12171  pcxcl  12855  pcdvdsb  12864  pcaddlem  12883  pcadd  12884  xblss2ps  15099  xblss2  15100  blss2ps  15101  blss2  15102  blhalf  15103  cnblcld  15230  ioo2blex  15247  tgioo  15249  cnopnap  15306  suplociccreex  15319  suplociccex  15320  dedekindicc  15328  ivthinclemlm  15329  ivthinclemum  15330  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthdec  15339  ivthreinc  15340  sin0pilem2  15477  pilem3  15478  vtxdgfifival  16077