Theorem rpred 9931

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℝ⁺crp 9888

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-in 3206  df-ss 3213  df-rp 9889

This theorem is referenced by:  rpxrd  9932  rpcnd  9933  rpregt0d  9938  rprege0d  9939  rprene0d  9940  rprecred  9943  ltmulgt11d  9967  ltmulgt12d  9968  gt0divd  9969  ge0divd  9970  lediv12ad  9991  ltexp2a  10854  leexp2a  10855  expnlbnd2  10928  cvg1nlemcxze  11544  cvg1nlemcau  11546  cvg1nlemres  11547  cvg1n  11548  resqrexlemp1rp  11568  resqrexlemfp1  11571  resqrexlemover  11572  resqrexlemdec  11573  resqrexlemdecn  11574  resqrexlemlo  11575  resqrexlemcalc1  11576  resqrexlemcalc2  11577  resqrexlemcalc3  11578  resqrexlemnmsq  11579  resqrexlemnm  11580  resqrexlemcvg  11581  resqrexlemgt0  11582  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemga  11585  cau3lem  11676  bdtrilem  11801  bdtri  11802  addcn2  11872  mulcn2  11874  reccn2ap  11875  climrecvg1n  11910  climcvg1nlem  11911  isumrpcl  12057  expcnvap0  12065  absgtap  12073  cvgratnnlemsumlt  12091  cvgratnnlemfm  12092  cvgratnnlemrate  12093  mertenslemi1  12098  effsumlt  12255  eirraplem  12340  bitsmod  12519  4sqlem7  12959  ssblex  15158  metss2lem  15224  addcncntoplem  15288  mulcncflem  15334  ivthinclemlopn  15363  ivthinclemuopn  15365  limcimolemlt  15391  limcimo  15392  cnplimclemle  15395  limccnp2lem  15403  dveflem  15453  efltlemlt  15501  pilem3  15510  cxplt  15643  cxple  15644  rpcxple2  15645  rpcxplt2  15646  rpcxpsqrt  15649  rpabscxpbnd  15667  logbgt0b  15693  logbgcd1irr  15694  logbgcd1irraplemexp  15695  qdencn  16652  cvgcmp2nlemabs  16657  iooref1o  16659  trilpolemclim  16661  trilpolemisumle  16663  trilpolemeq1  16665  nconstwlpolemgt0  16689  taupi  16698