Theorem rexrd 8376

Description: A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rexrd.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
rexrd	|- ( ph -> A e. RR* )

Proof of Theorem rexrd

Step	Hyp	Ref	Expression
1		ressxr 8370	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sselid 3246	1 |- ( ph -> A e. RR* )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   RR*cxr 8360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-xr 8365

This theorem is used by:  xnn0xr  9640  rpxr  10073  rpxrd  10109  xnn0dcle  10215  xnegcl  10245  xaddf  10257  xaddval  10258  xnn0lenn0nn0  10278  xposdif  10295  iooshf  10365  icoshftf1o  10404  ioo0  10705  ioom  10706  ico0  10707  ioc0  10708  xqltnle  10713  modqelico  10786  mulqaddmodid  10816  addmodid  10824  elicc4abs  11877  xrmaxiflemcl  12030  fprodge1  12425  pcxcl  13113  pcdvdsb  13122  pcaddlem  13141  pcadd  13142  xblss2ps  15596  xblss2  15597  blss2ps  15598  blss2  15599  blhalf  15600  cnblcld  15727  ioo2blex  15744  tgioo  15746  cnopnap  15803  suplociccreex  15816  suplociccex  15817  dedekindicc  15825  ivthinclemlm  15826  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthdec  15836  ivthreinc  15837  sin0pilem2  15975  pilem3  15976  vtxdgfifival  16698