Theorem rexrd 8071

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 8065	. 2 |- RR C_ RR*
2		rexrd.1	. 2 |- ( ph -> A e. RR )
3	1, 2	sselid 3178	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7873   RR*cxr 8055

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-xr 8060

This theorem is referenced by:  xnn0xr  9311  rpxr  9730  rpxrd  9766  xnn0dcle  9871  xnegcl  9901  xaddf  9913  xaddval  9914  xnn0lenn0nn0  9934  xposdif  9951  iooshf  10021  icoshftf1o  10060  ioo0  10331  ioom  10332  ico0  10333  ioc0  10334  xqltnle  10339  modqelico  10408  mulqaddmodid  10438  addmodid  10446  elicc4abs  11241  xrmaxiflemcl  11391  fprodge1  11785  pcxcl  12452  pcdvdsb  12461  pcaddlem  12480  pcadd  12481  xblss2ps  14583  xblss2  14584  blss2ps  14585  blss2  14586  blhalf  14587  cnblcld  14714  ioo2blex  14731  tgioo  14733  cnopnap  14790  suplociccreex  14803  suplociccex  14804  dedekindicc  14812  ivthinclemlm  14813  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthdec  14823  ivthreinc  14824  sin0pilem2  14958  pilem3  14959