Theorem rpred 9694

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

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

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 9652

This theorem is referenced by:  rpxrd  9695  rpcnd  9696  rpregt0d  9701  rprege0d  9702  rprene0d  9703  rprecred  9706  ltmulgt11d  9730  ltmulgt12d  9731  gt0divd  9732  ge0divd  9733  lediv12ad  9754  ltexp2a  10569  leexp2a  10570  expnlbnd2  10642  cvg1nlemcxze  10986  cvg1nlemcau  10988  cvg1nlemres  10989  cvg1n  10990  resqrexlemp1rp  11010  resqrexlemfp1  11013  resqrexlemover  11014  resqrexlemdec  11015  resqrexlemdecn  11016  resqrexlemlo  11017  resqrexlemcalc1  11018  resqrexlemcalc2  11019  resqrexlemcalc3  11020  resqrexlemnmsq  11021  resqrexlemnm  11022  resqrexlemcvg  11023  resqrexlemgt0  11024  resqrexlemoverl  11025  resqrexlemglsq  11026  resqrexlemga  11027  cau3lem  11118  bdtrilem  11242  bdtri  11243  addcn2  11313  mulcn2  11315  reccn2ap  11316  climrecvg1n  11351  climcvg1nlem  11352  isumrpcl  11497  expcnvap0  11505  absgtap  11513  cvgratnnlemsumlt  11531  cvgratnnlemfm  11532  cvgratnnlemrate  11533  mertenslemi1  11538  effsumlt  11695  eirraplem  11779  4sqlem7  12376  ssblex  13824  metss2lem  13890  addcncntoplem  13944  mulcncflem  13983  ivthinclemlopn  14007  ivthinclemuopn  14009  limcimolemlt  14026  limcimo  14027  cnplimclemle  14030  limccnp2lem  14038  dveflem  14080  efltlemlt  14088  pilem3  14097  cxplt  14229  cxple  14230  rpcxple2  14231  rpcxplt2  14232  rpcxpsqrt  14235  rpabscxpbnd  14252  logbgt0b  14277  logbgcd1irr  14278  logbgcd1irraplemexp  14279  qdencn  14657  cvgcmp2nlemabs  14662  iooref1o  14664  trilpolemclim  14666  trilpolemisumle  14668  trilpolemeq1  14670  nconstwlpolemgt0  14693  taupi  14702