Theorem rpred 8773

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

Syntax hints:   → wi 4   ∈ wcel 1433  ℝcr 6980  ℝ⁺crp 8734

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rab 2357  df-in 2979  df-ss 2986  df-rp 8735

This theorem is referenced by:  rpxrd  8774  rpcnd  8775  rpregt0d  8780  rprege0d  8781  rprene0d  8782  rprecred  8785  ltmulgt11d  8809  ltmulgt12d  8810  gt0divd  8811  ge0divd  8812  lediv12ad  8833  ltexp2a  9528  leexp2a  9529  expnlbnd2  9598  cvg1nlemcxze  9868  cvg1nlemcau  9870  cvg1nlemres  9871  cvg1n  9872  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemdecn  9898  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnmsq  9903  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  cau3lem  10000  addcn2  10149  mulcn2  10151  climrecvg1n  10185  climcvg1nlem  10186  qdencn  10785