Theorem rexrd 8207

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8009  ℝ^*cxr 8191

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 8196

This theorem is referenced by:  xnn0xr  9448  rpxr  9869  rpxrd  9905  xnn0dcle  10010  xnegcl  10040  xaddf  10052  xaddval  10053  xnn0lenn0nn0  10073  xposdif  10090  iooshf  10160  icoshftf1o  10199  ioo0  10491  ioom  10492  ico0  10493  ioc0  10494  xqltnle  10499  modqelico  10568  mulqaddmodid  10598  addmodid  10606  elicc4abs  11620  xrmaxiflemcl  11771  fprodge1  12165  pcxcl  12849  pcdvdsb  12858  pcaddlem  12877  pcadd  12878  xblss2ps  15093  xblss2  15094  blss2ps  15095  blss2  15096  blhalf  15097  cnblcld  15224  ioo2blex  15241  tgioo  15243  cnopnap  15300  suplociccreex  15313  suplociccex  15314  dedekindicc  15322  ivthinclemlm  15323  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthdec  15333  ivthreinc  15334  sin0pilem2  15471  pilem3  15472  vtxdgfifival  16050