Theorem rpred 10076

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

Syntax hints:   -> wi 4   e. wcel 2209   RRcr 8168   RR+crp 10033

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233  df-rp 10034

This theorem is referenced by:  rpxrd  10077  rpcnd  10078  rpregt0d  10083  rprege0d  10084  rprene0d  10085  rprecred  10088  ltmulgt11d  10112  ltmulgt12d  10113  gt0divd  10114  ge0divd  10115  lediv12ad  10136  ltexp2a  11006  leexp2a  11007  expnlbnd2  11081  cvg1nlemcxze  11726  cvg1nlemcau  11728  cvg1nlemres  11729  cvg1n  11730  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemdecn  11756  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemnmsq  11761  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  cau3lem  11858  bdtrilem  11983  bdtri  11984  addcn2  12054  mulcn2  12056  reccn2ap  12057  climrecvg1n  12092  climcvg1nlem  12093  isumrpcl  12239  expcnvap0  12247  absgtap  12255  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratnnlemrate  12275  mertenslemi1  12280  effsumlt  12437  eirraplem  12522  bitsmod  12701  4sqlem7  13141  ssblex  15455  metss2lem  15521  addcncntoplem  15585  mulcncflem  15631  ivthinclemlopn  15660  ivthinclemuopn  15662  limcimolemlt  15688  limcimo  15689  cnplimclemle  15692  limccnp2lem  15700  dveflem  15750  efltlemlt  15798  pilem3  15807  cxplt  15941  cxple  15942  rpcxple2  15943  rpcxplt2  15944  rpcxpsqrt  15947  rpabscxpbnd  15965  logbgt0b  15991  logbgcd1irr  15992  logbgcd1irraplemexp  15993  qdencn  16977  cvgcmp2nlemabs  16986  iooref1o  16988  trilpolemclim  16990  trilpolemisumle  16992  trilpolemeq1  16994  nconstwlpolemgt0  17019  taupi  17028