Theorem rexrd 8124

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7926   RR*cxr 8108

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-xr 8113

This theorem is referenced by:  xnn0xr  9365  rpxr  9785  rpxrd  9821  xnn0dcle  9926  xnegcl  9956  xaddf  9968  xaddval  9969  xnn0lenn0nn0  9989  xposdif  10006  iooshf  10076  icoshftf1o  10115  ioo0  10404  ioom  10405  ico0  10406  ioc0  10407  xqltnle  10412  modqelico  10481  mulqaddmodid  10511  addmodid  10519  elicc4abs  11438  xrmaxiflemcl  11589  fprodge1  11983  pcxcl  12667  pcdvdsb  12676  pcaddlem  12695  pcadd  12696  xblss2ps  14909  xblss2  14910  blss2ps  14911  blss2  14912  blhalf  14913  cnblcld  15040  ioo2blex  15057  tgioo  15059  cnopnap  15116  suplociccreex  15129  suplociccex  15130  dedekindicc  15138  ivthinclemlm  15139  ivthinclemum  15140  ivthinclemlopn  15141  ivthinclemuopn  15143  ivthdec  15149  ivthreinc  15150  sin0pilem2  15287  pilem3  15288