Theorem rpxr 9622

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

Syntax hints:   -> wi 4   e. wcel 2142   RR*cxr 7957   RR+crp 9614

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 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-rab 2458  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-xr 7962  df-rp 9615

This theorem is referenced by:  xrminrpcl  11241  blcntrps  13294  blcntr  13295  unirnblps  13301  unirnbl  13302  blssexps  13308  blssex  13309  blin2  13311  neibl  13370  blnei  13371  metss  13373  metss2lem  13376  bdmet  13381  bdmopn  13383  mopnex  13384  metrest  13385  xmettx  13389  metcnp3  13390  metcnp  13391  metcnpi3  13396  txmetcnp  13397  limcimolemlt  13512