Theorem rpred 9609

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

Syntax hints:   -> wi 4   e. wcel 2128   RRcr 7733   RR+crp 9566

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-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rab 2444  df-in 3108  df-ss 3115  df-rp 9567

This theorem is referenced by:  rpxrd  9610  rpcnd  9611  rpregt0d  9616  rprege0d  9617  rprene0d  9618  rprecred  9621  ltmulgt11d  9645  ltmulgt12d  9646  gt0divd  9647  ge0divd  9648  lediv12ad  9669  ltexp2a  10480  leexp2a  10481  expnlbnd2  10552  cvg1nlemcxze  10893  cvg1nlemcau  10895  cvg1nlemres  10896  cvg1n  10897  resqrexlemp1rp  10917  resqrexlemfp1  10920  resqrexlemover  10921  resqrexlemdec  10922  resqrexlemdecn  10923  resqrexlemlo  10924  resqrexlemcalc1  10925  resqrexlemcalc2  10926  resqrexlemcalc3  10927  resqrexlemnmsq  10928  resqrexlemnm  10929  resqrexlemcvg  10930  resqrexlemgt0  10931  resqrexlemoverl  10932  resqrexlemglsq  10933  resqrexlemga  10934  cau3lem  11025  bdtrilem  11149  bdtri  11150  addcn2  11218  mulcn2  11220  reccn2ap  11221  climrecvg1n  11256  climcvg1nlem  11257  isumrpcl  11402  expcnvap0  11410  absgtap  11418  cvgratnnlemsumlt  11436  cvgratnnlemfm  11437  cvgratnnlemrate  11438  mertenslemi1  11443  effsumlt  11600  eirraplem  11684  ssblex  12901  metss2lem  12967  addcncntoplem  13021  mulcncflem  13060  ivthinclemlopn  13084  ivthinclemuopn  13086  limcimolemlt  13103  limcimo  13104  cnplimclemle  13107  limccnp2lem  13115  dveflem  13157  efltlemlt  13165  pilem3  13174  cxplt  13306  cxple  13307  rpcxple2  13308  rpcxplt2  13309  rpcxpsqrt  13312  rpabscxpbnd  13329  logbgt0b  13354  logbgcd1irr  13355  logbgcd1irraplemexp  13356  qdencn  13669  cvgcmp2nlemabs  13674  iooref1o  13676  trilpolemclim  13678  trilpolemisumle  13680  trilpolemeq1  13682  nconstwlpolemgt0  13705  taupi  13712