Theorem rpred 9931

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 9899	. 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 8031   RR+crp 9888

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 9889

This theorem is referenced by:  rpxrd  9932  rpcnd  9933  rpregt0d  9938  rprege0d  9939  rprene0d  9940  rprecred  9943  ltmulgt11d  9967  ltmulgt12d  9968  gt0divd  9969  ge0divd  9970  lediv12ad  9991  ltexp2a  10854  leexp2a  10855  expnlbnd2  10928  cvg1nlemcxze  11560  cvg1nlemcau  11562  cvg1nlemres  11563  cvg1n  11564  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrexlemover  11588  resqrexlemdec  11589  resqrexlemdecn  11590  resqrexlemlo  11591  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnmsq  11595  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemga  11601  cau3lem  11692  bdtrilem  11817  bdtri  11818  addcn2  11888  mulcn2  11890  reccn2ap  11891  climrecvg1n  11926  climcvg1nlem  11927  isumrpcl  12073  expcnvap0  12081  absgtap  12089  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  cvgratnnlemrate  12109  mertenslemi1  12114  effsumlt  12271  eirraplem  12356  bitsmod  12535  4sqlem7  12975  ssblex  15174  metss2lem  15240  addcncntoplem  15304  mulcncflem  15350  ivthinclemlopn  15379  ivthinclemuopn  15381  limcimolemlt  15407  limcimo  15408  cnplimclemle  15411  limccnp2lem  15419  dveflem  15469  efltlemlt  15517  pilem3  15526  cxplt  15659  cxple  15660  rpcxple2  15661  rpcxplt2  15662  rpcxpsqrt  15665  rpabscxpbnd  15683  logbgt0b  15709  logbgcd1irr  15710  logbgcd1irraplemexp  15711  qdencn  16682  cvgcmp2nlemabs  16687  iooref1o  16689  trilpolemclim  16691  trilpolemisumle  16693  trilpolemeq1  16695  nconstwlpolemgt0  16720  taupi  16729