Theorem rpred 9171

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 9142	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sseldi 3023	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1438   RRcr 7347   RR+crp 9132

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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rab 2368  df-in 3005  df-ss 3012  df-rp 9133

This theorem is referenced by:  rpxrd  9172  rpcnd  9173  rpregt0d  9178  rprege0d  9179  rprene0d  9180  rprecred  9183  ltmulgt11d  9207  ltmulgt12d  9208  gt0divd  9209  ge0divd  9210  lediv12ad  9231  ltexp2a  10003  leexp2a  10004  expnlbnd2  10075  cvg1nlemcxze  10411  cvg1nlemcau  10413  cvg1nlemres  10414  cvg1n  10415  resqrexlemp1rp  10435  resqrexlemfp1  10438  resqrexlemover  10439  resqrexlemdec  10440  resqrexlemdecn  10441  resqrexlemlo  10442  resqrexlemcalc1  10443  resqrexlemcalc2  10444  resqrexlemcalc3  10445  resqrexlemnmsq  10446  resqrexlemnm  10447  resqrexlemcvg  10448  resqrexlemgt0  10449  resqrexlemoverl  10450  resqrexlemglsq  10451  resqrexlemga  10452  cau3lem  10543  addcn2  10695  mulcn2  10697  climrecvg1n  10733  climcvg1nlem  10734  isumrpcl  10884  expcnvap0  10892  absgtap  10900  cvgratnnlemsumlt  10918  cvgratnnlemfm  10919  cvgratnnlemrate  10920  mertenslemi1  10925  effsumlt  10978  eirraplem  11060  qdencn  11870