Theorem rexrd 8229

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   RR*cxr 8213

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-xr 8218

This theorem is referenced by:  xnn0xr  9470  rpxr  9896  rpxrd  9932  xnn0dcle  10037  xnegcl  10067  xaddf  10079  xaddval  10080  xnn0lenn0nn0  10100  xposdif  10117  iooshf  10187  icoshftf1o  10226  ioo0  10520  ioom  10521  ico0  10522  ioc0  10523  xqltnle  10528  modqelico  10597  mulqaddmodid  10627  addmodid  10635  elicc4abs  11656  xrmaxiflemcl  11807  fprodge1  12202  pcxcl  12886  pcdvdsb  12895  pcaddlem  12914  pcadd  12915  xblss2ps  15131  xblss2  15132  blss2ps  15133  blss2  15134  blhalf  15135  cnblcld  15262  ioo2blex  15279  tgioo  15281  cnopnap  15338  suplociccreex  15351  suplociccex  15352  dedekindicc  15360  ivthinclemlm  15361  ivthinclemum  15362  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthdec  15371  ivthreinc  15372  sin0pilem2  15509  pilem3  15510  vtxdgfifival  16145