Theorem rpred 9924

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  ℝ⁺crp 9881

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-in 3204  df-ss 3211  df-rp 9882

This theorem is referenced by:  rpxrd  9925  rpcnd  9926  rpregt0d  9931  rprege0d  9932  rprene0d  9933  rprecred  9936  ltmulgt11d  9960  ltmulgt12d  9961  gt0divd  9962  ge0divd  9963  lediv12ad  9984  ltexp2a  10846  leexp2a  10847  expnlbnd2  10920  cvg1nlemcxze  11536  cvg1nlemcau  11538  cvg1nlemres  11539  cvg1n  11540  resqrexlemp1rp  11560  resqrexlemfp1  11563  resqrexlemover  11564  resqrexlemdec  11565  resqrexlemdecn  11566  resqrexlemlo  11567  resqrexlemcalc1  11568  resqrexlemcalc2  11569  resqrexlemcalc3  11570  resqrexlemnmsq  11571  resqrexlemnm  11572  resqrexlemcvg  11573  resqrexlemgt0  11574  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemga  11577  cau3lem  11668  bdtrilem  11793  bdtri  11794  addcn2  11864  mulcn2  11866  reccn2ap  11867  climrecvg1n  11902  climcvg1nlem  11903  isumrpcl  12048  expcnvap0  12056  absgtap  12064  cvgratnnlemsumlt  12082  cvgratnnlemfm  12083  cvgratnnlemrate  12084  mertenslemi1  12089  effsumlt  12246  eirraplem  12331  bitsmod  12510  4sqlem7  12950  ssblex  15148  metss2lem  15214  addcncntoplem  15278  mulcncflem  15324  ivthinclemlopn  15353  ivthinclemuopn  15355  limcimolemlt  15381  limcimo  15382  cnplimclemle  15385  limccnp2lem  15393  dveflem  15443  efltlemlt  15491  pilem3  15500  cxplt  15633  cxple  15634  rpcxple2  15635  rpcxplt2  15636  rpcxpsqrt  15639  rpabscxpbnd  15657  logbgt0b  15683  logbgcd1irr  15684  logbgcd1irraplemexp  15685  qdencn  16581  cvgcmp2nlemabs  16586  iooref1o  16588  trilpolemclim  16590  trilpolemisumle  16592  trilpolemeq1  16594  nconstwlpolemgt0  16618  taupi  16627