Theorem rexrd 8020

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

Syntax hints:   -> wi 4   e. wcel 2158   RRcr 7823   RR*cxr 8004

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-xr 8009

This theorem is referenced by:  xnn0xr  9257  rpxr  9674  rpxrd  9710  xnn0dcle  9815  xnegcl  9845  xaddf  9857  xaddval  9858  xnn0lenn0nn0  9878  xposdif  9895  iooshf  9965  icoshftf1o  10004  ioo0  10273  ioom  10274  ico0  10275  ioc0  10276  modqelico  10347  mulqaddmodid  10377  addmodid  10385  elicc4abs  11116  xrmaxiflemcl  11266  fprodge1  11660  pcxcl  12324  pcdvdsb  12332  pcaddlem  12351  pcadd  12352  xblss2ps  14175  xblss2  14176  blss2ps  14177  blss2  14178  blhalf  14179  cnblcld  14306  ioo2blex  14315  tgioo  14317  cnopnap  14365  suplociccreex  14373  suplociccex  14374  dedekindicc  14382  ivthinclemlm  14383  ivthinclemum  14384  ivthinclemlopn  14385  ivthinclemuopn  14387  ivthdec  14393  sin0pilem2  14474  pilem3  14475