Theorem rpred 9817

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

Syntax hints:   -> wi 4   e. wcel 2175   RRcr 7923   RR+crp 9774

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-in 3171  df-ss 3178  df-rp 9775

This theorem is referenced by:  rpxrd  9818  rpcnd  9819  rpregt0d  9824  rprege0d  9825  rprene0d  9826  rprecred  9829  ltmulgt11d  9853  ltmulgt12d  9854  gt0divd  9855  ge0divd  9856  lediv12ad  9877  ltexp2a  10734  leexp2a  10735  expnlbnd2  10808  cvg1nlemcxze  11264  cvg1nlemcau  11266  cvg1nlemres  11267  cvg1n  11268  resqrexlemp1rp  11288  resqrexlemfp1  11291  resqrexlemover  11292  resqrexlemdec  11293  resqrexlemdecn  11294  resqrexlemlo  11295  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrexlemcalc3  11298  resqrexlemnmsq  11299  resqrexlemnm  11300  resqrexlemcvg  11301  resqrexlemgt0  11302  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemga  11305  cau3lem  11396  bdtrilem  11521  bdtri  11522  addcn2  11592  mulcn2  11594  reccn2ap  11595  climrecvg1n  11630  climcvg1nlem  11631  isumrpcl  11776  expcnvap0  11784  absgtap  11792  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratnnlemrate  11812  mertenslemi1  11817  effsumlt  11974  eirraplem  12059  bitsmod  12238  4sqlem7  12678  ssblex  14874  metss2lem  14940  addcncntoplem  15004  mulcncflem  15050  ivthinclemlopn  15079  ivthinclemuopn  15081  limcimolemlt  15107  limcimo  15108  cnplimclemle  15111  limccnp2lem  15119  dveflem  15169  efltlemlt  15217  pilem3  15226  cxplt  15359  cxple  15360  rpcxple2  15361  rpcxplt2  15362  rpcxpsqrt  15365  rpabscxpbnd  15383  logbgt0b  15409  logbgcd1irr  15410  logbgcd1irraplemexp  15411  qdencn  15928  cvgcmp2nlemabs  15933  iooref1o  15935  trilpolemclim  15937  trilpolemisumle  15939  trilpolemeq1  15941  nconstwlpolemgt0  15965  taupi  15974