Theorem rpred 9904

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 9872	. 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 8009   RR+crp 9861

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 9862

This theorem is referenced by:  rpxrd  9905  rpcnd  9906  rpregt0d  9911  rprege0d  9912  rprene0d  9913  rprecred  9916  ltmulgt11d  9940  ltmulgt12d  9941  gt0divd  9942  ge0divd  9943  lediv12ad  9964  ltexp2a  10825  leexp2a  10826  expnlbnd2  10899  cvg1nlemcxze  11508  cvg1nlemcau  11510  cvg1nlemres  11511  cvg1n  11512  resqrexlemp1rp  11532  resqrexlemfp1  11535  resqrexlemover  11536  resqrexlemdec  11537  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemgt0  11546  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  cau3lem  11640  bdtrilem  11765  bdtri  11766  addcn2  11836  mulcn2  11838  reccn2ap  11839  climrecvg1n  11874  climcvg1nlem  11875  isumrpcl  12020  expcnvap0  12028  absgtap  12036  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  mertenslemi1  12061  effsumlt  12218  eirraplem  12303  bitsmod  12482  4sqlem7  12922  ssblex  15120  metss2lem  15186  addcncntoplem  15250  mulcncflem  15296  ivthinclemlopn  15325  ivthinclemuopn  15327  limcimolemlt  15353  limcimo  15354  cnplimclemle  15357  limccnp2lem  15365  dveflem  15415  efltlemlt  15463  pilem3  15472  cxplt  15605  cxple  15606  rpcxple2  15607  rpcxplt2  15608  rpcxpsqrt  15611  rpabscxpbnd  15629  logbgt0b  15655  logbgcd1irr  15656  logbgcd1irraplemexp  15657  qdencn  16455  cvgcmp2nlemabs  16460  iooref1o  16462  trilpolemclim  16464  trilpolemisumle  16466  trilpolemeq1  16468  nconstwlpolemgt0  16492  taupi  16501