Theorem rpred 9936

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℝcr 8036  ℝ⁺crp 9893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rab 2518  df-in 3205  df-ss 3212  df-rp 9894

This theorem is referenced by:  rpxrd  9937  rpcnd  9938  rpregt0d  9943  rprege0d  9944  rprene0d  9945  rprecred  9948  ltmulgt11d  9972  ltmulgt12d  9973  gt0divd  9974  ge0divd  9975  lediv12ad  9996  ltexp2a  10859  leexp2a  10860  expnlbnd2  10933  cvg1nlemcxze  11565  cvg1nlemcau  11567  cvg1nlemres  11568  cvg1n  11569  resqrexlemp1rp  11589  resqrexlemfp1  11592  resqrexlemover  11593  resqrexlemdec  11594  resqrexlemdecn  11595  resqrexlemlo  11596  resqrexlemcalc1  11597  resqrexlemcalc2  11598  resqrexlemcalc3  11599  resqrexlemnmsq  11600  resqrexlemnm  11601  resqrexlemcvg  11602  resqrexlemgt0  11603  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemga  11606  cau3lem  11697  bdtrilem  11822  bdtri  11823  addcn2  11893  mulcn2  11895  reccn2ap  11896  climrecvg1n  11931  climcvg1nlem  11932  isumrpcl  12078  expcnvap0  12086  absgtap  12094  cvgratnnlemsumlt  12112  cvgratnnlemfm  12113  cvgratnnlemrate  12114  mertenslemi1  12119  effsumlt  12276  eirraplem  12361  bitsmod  12540  4sqlem7  12980  ssblex  15184  metss2lem  15250  addcncntoplem  15314  mulcncflem  15360  ivthinclemlopn  15389  ivthinclemuopn  15391  limcimolemlt  15417  limcimo  15418  cnplimclemle  15421  limccnp2lem  15429  dveflem  15479  efltlemlt  15527  pilem3  15536  cxplt  15669  cxple  15670  rpcxple2  15671  rpcxplt2  15672  rpcxpsqrt  15675  rpabscxpbnd  15693  logbgt0b  15719  logbgcd1irr  15720  logbgcd1irraplemexp  15721  qdencn  16694  cvgcmp2nlemabs  16703  iooref1o  16705  trilpolemclim  16707  trilpolemisumle  16709  trilpolemeq1  16711  nconstwlpolemgt0  16736  taupi  16745