Theorem rpxr 9896

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

Assertion

Ref	Expression
rpxr	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Proof of Theorem rpxr

Step	Hyp	Ref	Expression
1		rpre 9895	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	rexrd 8229	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝ^*cxr 8213  ℝ⁺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  11836  blcntrps  15142  blcntr  15143  unirnblps  15149  unirnbl  15150  blssexps  15156  blssex  15157  blin2  15159  neibl  15218  blnei  15219  metss  15221  metss2lem  15224  bdmet  15229  bdmopn  15231  mopnex  15232  metrest  15233  xmettx  15237  metcnp3  15238  metcnp  15239  metcnpi3  15244  txmetcnp  15245  limcimolemlt  15391