Theorem rpred 9695

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7809  ℝ⁺crp 9652

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 3135  df-ss 3142  df-rp 9653

This theorem is referenced by:  rpxrd  9696  rpcnd  9697  rpregt0d  9702  rprege0d  9703  rprene0d  9704  rprecred  9707  ltmulgt11d  9731  ltmulgt12d  9732  gt0divd  9733  ge0divd  9734  lediv12ad  9755  ltexp2a  10571  leexp2a  10572  expnlbnd2  10645  cvg1nlemcxze  10990  cvg1nlemcau  10992  cvg1nlemres  10993  cvg1n  10994  resqrexlemp1rp  11014  resqrexlemfp1  11017  resqrexlemover  11018  resqrexlemdec  11019  resqrexlemdecn  11020  resqrexlemlo  11021  resqrexlemcalc1  11022  resqrexlemcalc2  11023  resqrexlemcalc3  11024  resqrexlemnmsq  11025  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemgt0  11028  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  cau3lem  11122  bdtrilem  11246  bdtri  11247  addcn2  11317  mulcn2  11319  reccn2ap  11320  climrecvg1n  11355  climcvg1nlem  11356  isumrpcl  11501  expcnvap0  11509  absgtap  11517  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  mertenslemi1  11542  effsumlt  11699  eirraplem  11783  4sqlem7  12381  ssblex  13901  metss2lem  13967  addcncntoplem  14021  mulcncflem  14060  ivthinclemlopn  14084  ivthinclemuopn  14086  limcimolemlt  14103  limcimo  14104  cnplimclemle  14107  limccnp2lem  14115  dveflem  14157  efltlemlt  14165  pilem3  14174  cxplt  14306  cxple  14307  rpcxple2  14308  rpcxplt2  14309  rpcxpsqrt  14312  rpabscxpbnd  14329  logbgt0b  14354  logbgcd1irr  14355  logbgcd1irraplemexp  14356  qdencn  14745  cvgcmp2nlemabs  14750  iooref1o  14752  trilpolemclim  14754  trilpolemisumle  14756  trilpolemeq1  14758  nconstwlpolemgt0  14781  taupi  14790