Theorem rpred 9771

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 9739	. 2 ⊢ ℝ+ ⊆ ℝ
2		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
3	1, 2	sselid 3181	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7878  ℝ⁺crp 9728

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-in 3163  df-ss 3170  df-rp 9729

This theorem is referenced by:  rpxrd  9772  rpcnd  9773  rpregt0d  9778  rprege0d  9779  rprene0d  9780  rprecred  9783  ltmulgt11d  9807  ltmulgt12d  9808  gt0divd  9809  ge0divd  9810  lediv12ad  9831  ltexp2a  10683  leexp2a  10684  expnlbnd2  10757  cvg1nlemcxze  11147  cvg1nlemcau  11149  cvg1nlemres  11150  cvg1n  11151  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrexlemover  11175  resqrexlemdec  11176  resqrexlemdecn  11177  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  cau3lem  11279  bdtrilem  11404  bdtri  11405  addcn2  11475  mulcn2  11477  reccn2ap  11478  climrecvg1n  11513  climcvg1nlem  11514  isumrpcl  11659  expcnvap0  11667  absgtap  11675  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  mertenslemi1  11700  effsumlt  11857  eirraplem  11942  4sqlem7  12553  ssblex  14667  metss2lem  14733  addcncntoplem  14797  mulcncflem  14843  ivthinclemlopn  14872  ivthinclemuopn  14874  limcimolemlt  14900  limcimo  14901  cnplimclemle  14904  limccnp2lem  14912  dveflem  14962  efltlemlt  15010  pilem3  15019  cxplt  15152  cxple  15153  rpcxple2  15154  rpcxplt2  15155  rpcxpsqrt  15158  rpabscxpbnd  15176  logbgt0b  15202  logbgcd1irr  15203  logbgcd1irraplemexp  15204  qdencn  15671  cvgcmp2nlemabs  15676  iooref1o  15678  trilpolemclim  15680  trilpolemisumle  15682  trilpolemeq1  15684  nconstwlpolemgt0  15708  taupi  15717