Theorem rpred 9696

Description: A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem rpred

Step	Hyp	Ref	Expression
1		rpssre 9664	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3154	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7810  ℝ⁺crp 9653

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-in 3136  df-ss 3143  df-rp 9654

This theorem is referenced by:  rpxrd  9697  rpcnd  9698  rpregt0d  9703  rprege0d  9704  rprene0d  9705  rprecred  9708  ltmulgt11d  9732  ltmulgt12d  9733  gt0divd  9734  ge0divd  9735  lediv12ad  9756  ltexp2a  10572  leexp2a  10573  expnlbnd2  10646  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  cvg1n  10995  resqrexlemp1rp  11015  resqrexlemfp1  11018  resqrexlemover  11019  resqrexlemdec  11020  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnmsq  11026  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemga  11032  cau3lem  11123  bdtrilem  11247  bdtri  11248  addcn2  11318  mulcn2  11320  reccn2ap  11321  climrecvg1n  11356  climcvg1nlem  11357  isumrpcl  11502  expcnvap0  11510  absgtap  11518  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  mertenslemi1  11543  effsumlt  11700  eirraplem  11784  4sqlem7  12382  ssblex  13934  metss2lem  14000  addcncntoplem  14054  mulcncflem  14093  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimolemlt  14136  limcimo  14137  cnplimclemle  14140  limccnp2lem  14148  dveflem  14190  efltlemlt  14198  pilem3  14207  cxplt  14339  cxple  14340  rpcxple2  14341  rpcxplt2  14342  rpcxpsqrt  14345  rpabscxpbnd  14362  logbgt0b  14387  logbgcd1irr  14388  logbgcd1irraplemexp  14389  qdencn  14778  cvgcmp2nlemabs  14783  iooref1o  14785  trilpolemclim  14787  trilpolemisumle  14789  trilpolemeq1  14791  nconstwlpolemgt0  14814  taupi  14823