Theorem rpred 9930

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8030   RR+crp 9887

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-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213  df-rp 9888

This theorem is referenced by:  rpxrd  9931  rpcnd  9932  rpregt0d  9937  rprege0d  9938  rprene0d  9939  rprecred  9942  ltmulgt11d  9966  ltmulgt12d  9967  gt0divd  9968  ge0divd  9969  lediv12ad  9990  ltexp2a  10852  leexp2a  10853  expnlbnd2  10926  cvg1nlemcxze  11542  cvg1nlemcau  11544  cvg1nlemres  11545  cvg1n  11546  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnmsq  11577  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  cau3lem  11674  bdtrilem  11799  bdtri  11800  addcn2  11870  mulcn2  11872  reccn2ap  11873  climrecvg1n  11908  climcvg1nlem  11909  isumrpcl  12054  expcnvap0  12062  absgtap  12070  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  mertenslemi1  12095  effsumlt  12252  eirraplem  12337  bitsmod  12516  4sqlem7  12956  ssblex  15154  metss2lem  15220  addcncntoplem  15284  mulcncflem  15330  ivthinclemlopn  15359  ivthinclemuopn  15361  limcimolemlt  15387  limcimo  15388  cnplimclemle  15391  limccnp2lem  15399  dveflem  15449  efltlemlt  15497  pilem3  15506  cxplt  15639  cxple  15640  rpcxple2  15641  rpcxplt2  15642  rpcxpsqrt  15645  rpabscxpbnd  15663  logbgt0b  15689  logbgcd1irr  15690  logbgcd1irraplemexp  15691  qdencn  16631  cvgcmp2nlemabs  16636  iooref1o  16638  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  nconstwlpolemgt0  16668  taupi  16677