Theorem rpred 9628

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 9596	. 2 |- RR+ C_ RR
2		rpred.1	. 2 |- ( ph -> A e. RR+ )
3	1, 2	sselid 3139	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2136   RRcr 7748   RR+crp 9585

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rab 2452  df-in 3121  df-ss 3128  df-rp 9586

This theorem is referenced by:  rpxrd  9629  rpcnd  9630  rpregt0d  9635  rprege0d  9636  rprene0d  9637  rprecred  9640  ltmulgt11d  9664  ltmulgt12d  9665  gt0divd  9666  ge0divd  9667  lediv12ad  9688  ltexp2a  10503  leexp2a  10504  expnlbnd2  10576  cvg1nlemcxze  10920  cvg1nlemcau  10922  cvg1nlemres  10923  cvg1n  10924  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrexlemover  10948  resqrexlemdec  10949  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc1  10952  resqrexlemcalc2  10953  resqrexlemcalc3  10954  resqrexlemnmsq  10955  resqrexlemnm  10956  resqrexlemcvg  10957  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  cau3lem  11052  bdtrilem  11176  bdtri  11177  addcn2  11247  mulcn2  11249  reccn2ap  11250  climrecvg1n  11285  climcvg1nlem  11286  isumrpcl  11431  expcnvap0  11439  absgtap  11447  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  cvgratnnlemrate  11467  mertenslemi1  11472  effsumlt  11629  eirraplem  11713  4sqlem7  12310  ssblex  13031  metss2lem  13097  addcncntoplem  13151  mulcncflem  13190  ivthinclemlopn  13214  ivthinclemuopn  13216  limcimolemlt  13233  limcimo  13234  cnplimclemle  13237  limccnp2lem  13245  dveflem  13287  efltlemlt  13295  pilem3  13304  cxplt  13436  cxple  13437  rpcxple2  13438  rpcxplt2  13439  rpcxpsqrt  13442  rpabscxpbnd  13459  logbgt0b  13484  logbgcd1irr  13485  logbgcd1irraplemexp  13486  qdencn  13866  cvgcmp2nlemabs  13871  iooref1o  13873  trilpolemclim  13875  trilpolemisumle  13877  trilpolemeq1  13879  nconstwlpolemgt0  13902  taupi  13909