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  11672  xrmaxiflemcl  11823  fprodge1  12218  pcxcl  12902  pcdvdsb  12911  pcaddlem  12930  pcadd  12931  xblss2ps  15147  xblss2  15148  blss2ps  15149  blss2  15150  blhalf  15151  cnblcld  15278  ioo2blex  15295  tgioo  15297  cnopnap  15354  suplociccreex  15367  suplociccex  15368  dedekindicc  15376  ivthinclemlm  15377  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthdec  15387  ivthreinc  15388  sin0pilem2  15525  pilem3  15526  vtxdgfifival  16161