Theorem rpred 10025

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8122  ℝ⁺crp 9982

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rab 2529  df-in 3216  df-ss 3223  df-rp 9983

This theorem is referenced by:  rpxrd  10026  rpcnd  10027  rpregt0d  10032  rprege0d  10033  rprene0d  10034  rprecred  10037  ltmulgt11d  10061  ltmulgt12d  10062  gt0divd  10063  ge0divd  10064  lediv12ad  10085  ltexp2a  10949  leexp2a  10950  expnlbnd2  11023  cvg1nlemcxze  11660  cvg1nlemcau  11662  cvg1nlemres  11663  cvg1n  11664  resqrexlemp1rp  11684  resqrexlemfp1  11687  resqrexlemover  11688  resqrexlemdec  11689  resqrexlemdecn  11690  resqrexlemlo  11691  resqrexlemcalc1  11692  resqrexlemcalc2  11693  resqrexlemcalc3  11694  resqrexlemnmsq  11695  resqrexlemnm  11696  resqrexlemcvg  11697  resqrexlemgt0  11698  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemga  11701  cau3lem  11792  bdtrilem  11917  bdtri  11918  addcn2  11988  mulcn2  11990  reccn2ap  11991  climrecvg1n  12026  climcvg1nlem  12027  isumrpcl  12173  expcnvap0  12181  absgtap  12189  cvgratnnlemsumlt  12207  cvgratnnlemfm  12208  cvgratnnlemrate  12209  mertenslemi1  12214  effsumlt  12371  eirraplem  12456  bitsmod  12635  4sqlem7  13075  ssblex  15283  metss2lem  15349  addcncntoplem  15413  mulcncflem  15459  ivthinclemlopn  15488  ivthinclemuopn  15490  limcimolemlt  15516  limcimo  15517  cnplimclemle  15520  limccnp2lem  15528  dveflem  15578  efltlemlt  15626  pilem3  15635  cxplt  15768  cxple  15769  rpcxple2  15770  rpcxplt2  15771  rpcxpsqrt  15774  rpabscxpbnd  15792  logbgt0b  15818  logbgcd1irr  15819  logbgcd1irraplemexp  15820  qdencn  16794  cvgcmp2nlemabs  16803  iooref1o  16805  trilpolemclim  16807  trilpolemisumle  16809  trilpolemeq1  16811  nconstwlpolemgt0  16836  taupi  16845