Theorem rpred 8622

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

Syntax hints:   → wi 4   ∈ wcel 1393  ℝcr 6888  ℝ⁺crp 8583

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rab 2315  df-in 2924  df-ss 2931  df-rp 8584

This theorem is referenced by:  rpxrd  8623  rpcnd  8624  rpregt0d  8629  rprege0d  8630  rprene0d  8631  rprecred  8634  ltmulgt11d  8658  ltmulgt12d  8659  gt0divd  8660  ge0divd  8661  lediv12ad  8682  ltexp2a  9306  leexp2a  9307  expnlbnd2  9374  cvg1nlemcxze  9581  cvg1nlemcau  9583  cvg1nlemres  9584  cvg1n  9585  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  cau3lem  9710  addcn2  9831  mulcn2  9833  climrecvg1n  9867  climcvg1nlem  9868  qdencn  10124