Theorem rpred 9227

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

Syntax hints:   → wi 4   ∈ wcel 1439  ℝcr 7403  ℝ⁺crp 9188

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rab 2369  df-in 3006  df-ss 3013  df-rp 9189

This theorem is referenced by:  rpxrd  9228  rpcnd  9229  rpregt0d  9234  rprege0d  9235  rprene0d  9236  rprecred  9239  ltmulgt11d  9263  ltmulgt12d  9264  gt0divd  9265  ge0divd  9266  lediv12ad  9287  ltexp2a  10061  leexp2a  10062  expnlbnd2  10133  cvg1nlemcxze  10469  cvg1nlemcau  10471  cvg1nlemres  10472  cvg1n  10473  resqrexlemp1rp  10493  resqrexlemfp1  10496  resqrexlemover  10497  resqrexlemdec  10498  resqrexlemdecn  10499  resqrexlemlo  10500  resqrexlemcalc1  10501  resqrexlemcalc2  10502  resqrexlemcalc3  10503  resqrexlemnmsq  10504  resqrexlemnm  10505  resqrexlemcvg  10506  resqrexlemgt0  10507  resqrexlemoverl  10508  resqrexlemglsq  10509  resqrexlemga  10510  cau3lem  10601  addcn2  10753  mulcn2  10755  climrecvg1n  10791  climcvg1nlem  10792  isumrpcl  10942  expcnvap0  10950  absgtap  10958  cvgratnnlemsumlt  10976  cvgratnnlemfm  10977  cvgratnnlemrate  10978  mertenslemi1  10983  effsumlt  11036  eirraplem  11118  qdencn  12181