Theorem rpred 10080

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  ℝ⁺crp 10037

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-in 3226  df-ss 3233  df-rp 10038

This theorem is referenced by:  rpxrd  10081  rpcnd  10082  rpregt0d  10087  rprege0d  10088  rprene0d  10089  rprecred  10092  ltmulgt11d  10116  ltmulgt12d  10117  gt0divd  10118  ge0divd  10119  lediv12ad  10140  ltexp2a  11011  leexp2a  11012  expnlbnd2  11086  cvg1nlemcxze  11731  cvg1nlemcau  11733  cvg1nlemres  11734  cvg1n  11735  resqrexlemp1rp  11755  resqrexlemfp1  11758  resqrexlemover  11759  resqrexlemdec  11760  resqrexlemdecn  11761  resqrexlemlo  11762  resqrexlemcalc1  11763  resqrexlemcalc2  11764  resqrexlemcalc3  11765  resqrexlemnmsq  11766  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemgt0  11769  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemga  11772  cau3lem  11863  bdtrilem  11988  bdtri  11989  addcn2  12059  mulcn2  12061  reccn2ap  12062  climrecvg1n  12097  climcvg1nlem  12098  isumrpcl  12244  expcnvap0  12252  absgtap  12260  cvgratnnlemsumlt  12278  cvgratnnlemfm  12279  cvgratnnlemrate  12280  mertenslemi1  12285  effsumlt  12442  eirraplem  12527  bitsmod  12706  4sqlem7  13146  ssblex  15515  metss2lem  15581  addcncntoplem  15645  mulcncflem  15691  ivthinclemlopn  15720  ivthinclemuopn  15722  limcimolemlt  15748  limcimo  15749  cnplimclemle  15752  limccnp2lem  15760  dveflem  15810  efltlemlt  15858  pilem3  15867  cxplt  16001  cxple  16002  rpcxple2  16003  rpcxplt2  16004  rpcxpsqrt  16007  rpabscxpbnd  16025  logbgt0b  16051  logbgcd1irr  16052  logbgcd1irraplemexp  16053  log2tlbndlog2  16065  qdencn  17046  cvgcmp2nlemabs  17055  iooref1o  17057  trilpolemclim  17059  trilpolemisumle  17061  trilpolemeq1  17063  nconstwlpolemgt0  17088  taupi  17097