Theorem rpred 9653

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 7773  ℝ⁺crp 9610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rab 2457  df-in 3127  df-ss 3134  df-rp 9611

This theorem is referenced by:  rpxrd  9654  rpcnd  9655  rpregt0d  9660  rprege0d  9661  rprene0d  9662  rprecred  9665  ltmulgt11d  9689  ltmulgt12d  9690  gt0divd  9691  ge0divd  9692  lediv12ad  9713  ltexp2a  10528  leexp2a  10529  expnlbnd2  10601  cvg1nlemcxze  10946  cvg1nlemcau  10948  cvg1nlemres  10949  cvg1n  10950  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemnmsq  10981  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  cau3lem  11078  bdtrilem  11202  bdtri  11203  addcn2  11273  mulcn2  11275  reccn2ap  11276  climrecvg1n  11311  climcvg1nlem  11312  isumrpcl  11457  expcnvap0  11465  absgtap  11473  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratnnlemrate  11493  mertenslemi1  11498  effsumlt  11655  eirraplem  11739  4sqlem7  12336  ssblex  13225  metss2lem  13291  addcncntoplem  13345  mulcncflem  13384  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimolemlt  13427  limcimo  13428  cnplimclemle  13431  limccnp2lem  13439  dveflem  13481  efltlemlt  13489  pilem3  13498  cxplt  13630  cxple  13631  rpcxple2  13632  rpcxplt2  13633  rpcxpsqrt  13636  rpabscxpbnd  13653  logbgt0b  13678  logbgcd1irr  13679  logbgcd1irraplemexp  13680  qdencn  14059  cvgcmp2nlemabs  14064  iooref1o  14066  trilpolemclim  14068  trilpolemisumle  14070  trilpolemeq1  14072  nconstwlpolemgt0  14095  taupi  14102