Theorem rpred 9825

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7931  ℝ⁺crp 9782

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-in 3173  df-ss 3180  df-rp 9783

This theorem is referenced by:  rpxrd  9826  rpcnd  9827  rpregt0d  9832  rprege0d  9833  rprene0d  9834  rprecred  9837  ltmulgt11d  9861  ltmulgt12d  9862  gt0divd  9863  ge0divd  9864  lediv12ad  9885  ltexp2a  10743  leexp2a  10744  expnlbnd2  10817  cvg1nlemcxze  11337  cvg1nlemcau  11339  cvg1nlemres  11340  cvg1n  11341  resqrexlemp1rp  11361  resqrexlemfp1  11364  resqrexlemover  11365  resqrexlemdec  11366  resqrexlemdecn  11367  resqrexlemlo  11368  resqrexlemcalc1  11369  resqrexlemcalc2  11370  resqrexlemcalc3  11371  resqrexlemnmsq  11372  resqrexlemnm  11373  resqrexlemcvg  11374  resqrexlemgt0  11375  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemga  11378  cau3lem  11469  bdtrilem  11594  bdtri  11595  addcn2  11665  mulcn2  11667  reccn2ap  11668  climrecvg1n  11703  climcvg1nlem  11704  isumrpcl  11849  expcnvap0  11857  absgtap  11865  cvgratnnlemsumlt  11883  cvgratnnlemfm  11884  cvgratnnlemrate  11885  mertenslemi1  11890  effsumlt  12047  eirraplem  12132  bitsmod  12311  4sqlem7  12751  ssblex  14947  metss2lem  15013  addcncntoplem  15077  mulcncflem  15123  ivthinclemlopn  15152  ivthinclemuopn  15154  limcimolemlt  15180  limcimo  15181  cnplimclemle  15184  limccnp2lem  15192  dveflem  15242  efltlemlt  15290  pilem3  15299  cxplt  15432  cxple  15433  rpcxple2  15434  rpcxplt2  15435  rpcxpsqrt  15438  rpabscxpbnd  15456  logbgt0b  15482  logbgcd1irr  15483  logbgcd1irraplemexp  15484  qdencn  16040  cvgcmp2nlemabs  16045  iooref1o  16047  trilpolemclim  16049  trilpolemisumle  16051  trilpolemeq1  16053  nconstwlpolemgt0  16077  taupi  16086