Theorem rexrd 8093

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

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7895   RR*cxr 8077

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-xr 8082

This theorem is referenced by:  xnn0xr  9334  rpxr  9753  rpxrd  9789  xnn0dcle  9894  xnegcl  9924  xaddf  9936  xaddval  9937  xnn0lenn0nn0  9957  xposdif  9974  iooshf  10044  icoshftf1o  10083  ioo0  10366  ioom  10367  ico0  10368  ioc0  10369  xqltnle  10374  modqelico  10443  mulqaddmodid  10473  addmodid  10481  elicc4abs  11276  xrmaxiflemcl  11427  fprodge1  11821  pcxcl  12505  pcdvdsb  12514  pcaddlem  12533  pcadd  12534  xblss2ps  14724  xblss2  14725  blss2ps  14726  blss2  14727  blhalf  14728  cnblcld  14855  ioo2blex  14872  tgioo  14874  cnopnap  14931  suplociccreex  14944  suplociccex  14945  dedekindicc  14953  ivthinclemlm  14954  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthdec  14964  ivthreinc  14965  sin0pilem2  15102  pilem3  15103