Theorem rpred 9082

Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpred	|- ( ph -> A e. RR )

Proof of Theorem rpred

Step	Hyp	Ref	Expression
1		rpssre 9053	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sseldi 3010	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1436   RRcr 7270   RR+crp 9043

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rab 2364  df-in 2992  df-ss 2999  df-rp 9044

This theorem is referenced by:  rpxrd  9083  rpcnd  9084  rpregt0d  9089  rprege0d  9090  rprene0d  9091  rprecred  9094  ltmulgt11d  9118  ltmulgt12d  9119  gt0divd  9120  ge0divd  9121  lediv12ad  9142  ltexp2a  9858  leexp2a  9859  expnlbnd2  9928  cvg1nlemcxze  10256  cvg1nlemcau  10258  cvg1nlemres  10259  cvg1n  10260  resqrexlemp1rp  10280  resqrexlemfp1  10283  resqrexlemover  10284  resqrexlemdec  10285  resqrexlemdecn  10286  resqrexlemlo  10287  resqrexlemcalc1  10288  resqrexlemcalc2  10289  resqrexlemcalc3  10290  resqrexlemnmsq  10291  resqrexlemnm  10292  resqrexlemcvg  10293  resqrexlemgt0  10294  resqrexlemoverl  10295  resqrexlemglsq  10296  resqrexlemga  10297  cau3lem  10388  addcn2  10537  mulcn2  10539  climrecvg1n  10573  climcvg1nlem  10574  qdencn  11271