Theorem rpxr 9561

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 9560	. 2 |- ( A e. RR+ -> A e. RR )
2	1	rexrd 7921	1 |- ( A e. RR+ -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 2128   RR*cxr 7905   RR+crp 9553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-xr 7910  df-rp 9554

This theorem is referenced by:  xrminrpcl  11164  blcntrps  12786  blcntr  12787  unirnblps  12793  unirnbl  12794  blssexps  12800  blssex  12801  blin2  12803  neibl  12862  blnei  12863  metss  12865  metss2lem  12868  bdmet  12873  bdmopn  12875  mopnex  12876  metrest  12877  xmettx  12881  metcnp3  12882  metcnp  12883  metcnpi3  12888  txmetcnp  12889  limcimolemlt  13004