Theorem rpred 9888

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7994   RR+crp 9845

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3203  df-ss 3210  df-rp 9846

This theorem is referenced by:  rpxrd  9889  rpcnd  9890  rpregt0d  9895  rprege0d  9896  rprene0d  9897  rprecred  9900  ltmulgt11d  9924  ltmulgt12d  9925  gt0divd  9926  ge0divd  9927  lediv12ad  9948  ltexp2a  10808  leexp2a  10809  expnlbnd2  10882  cvg1nlemcxze  11488  cvg1nlemcau  11490  cvg1nlemres  11491  cvg1n  11492  resqrexlemp1rp  11512  resqrexlemfp1  11515  resqrexlemover  11516  resqrexlemdec  11517  resqrexlemdecn  11518  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemnmsq  11523  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  cau3lem  11620  bdtrilem  11745  bdtri  11746  addcn2  11816  mulcn2  11818  reccn2ap  11819  climrecvg1n  11854  climcvg1nlem  11855  isumrpcl  12000  expcnvap0  12008  absgtap  12016  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratnnlemrate  12036  mertenslemi1  12041  effsumlt  12198  eirraplem  12283  bitsmod  12462  4sqlem7  12902  ssblex  15099  metss2lem  15165  addcncntoplem  15229  mulcncflem  15275  ivthinclemlopn  15304  ivthinclemuopn  15306  limcimolemlt  15332  limcimo  15333  cnplimclemle  15336  limccnp2lem  15344  dveflem  15394  efltlemlt  15442  pilem3  15451  cxplt  15584  cxple  15585  rpcxple2  15586  rpcxplt2  15587  rpcxpsqrt  15590  rpabscxpbnd  15608  logbgt0b  15634  logbgcd1irr  15635  logbgcd1irraplemexp  15636  qdencn  16354  cvgcmp2nlemabs  16359  iooref1o  16361  trilpolemclim  16363  trilpolemisumle  16365  trilpolemeq1  16367  nconstwlpolemgt0  16391  taupi  16400