Theorem rpxr 9896

Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
rpxr	|- ( A e. RR+ -> A e. RR* )

Proof of Theorem rpxr

Step	Hyp	Ref	Expression
1		rpre 9895	. 2 |- ( A e. RR+ -> A e. RR )
2	1	rexrd 8229	1 |- ( A e. RR+ -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2202   RR*cxr 8213   RR+crp 9888

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-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-xr 8218  df-rp 9889

This theorem is referenced by:  xrminrpcl  11852  blcntrps  15158  blcntr  15159  unirnblps  15165  unirnbl  15166  blssexps  15172  blssex  15173  blin2  15175  neibl  15234  blnei  15235  metss  15237  metss2lem  15240  bdmet  15245  bdmopn  15247  mopnex  15248  metrest  15249  xmettx  15253  metcnp3  15254  metcnp  15255  metcnpi3  15260  txmetcnp  15261  limcimolemlt  15407