Theorem rpred 9860

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℝcr 7966  ℝ⁺crp 9817

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rab 2497  df-in 3183  df-ss 3190  df-rp 9818

This theorem is referenced by:  rpxrd  9861  rpcnd  9862  rpregt0d  9867  rprege0d  9868  rprene0d  9869  rprecred  9872  ltmulgt11d  9896  ltmulgt12d  9897  gt0divd  9898  ge0divd  9899  lediv12ad  9920  ltexp2a  10780  leexp2a  10781  expnlbnd2  10854  cvg1nlemcxze  11459  cvg1nlemcau  11461  cvg1nlemres  11462  cvg1n  11463  resqrexlemp1rp  11483  resqrexlemfp1  11486  resqrexlemover  11487  resqrexlemdec  11488  resqrexlemdecn  11489  resqrexlemlo  11490  resqrexlemcalc1  11491  resqrexlemcalc2  11492  resqrexlemcalc3  11493  resqrexlemnmsq  11494  resqrexlemnm  11495  resqrexlemcvg  11496  resqrexlemgt0  11497  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemga  11500  cau3lem  11591  bdtrilem  11716  bdtri  11717  addcn2  11787  mulcn2  11789  reccn2ap  11790  climrecvg1n  11825  climcvg1nlem  11826  isumrpcl  11971  expcnvap0  11979  absgtap  11987  cvgratnnlemsumlt  12005  cvgratnnlemfm  12006  cvgratnnlemrate  12007  mertenslemi1  12012  effsumlt  12169  eirraplem  12254  bitsmod  12433  4sqlem7  12873  ssblex  15070  metss2lem  15136  addcncntoplem  15200  mulcncflem  15246  ivthinclemlopn  15275  ivthinclemuopn  15277  limcimolemlt  15303  limcimo  15304  cnplimclemle  15307  limccnp2lem  15315  dveflem  15365  efltlemlt  15413  pilem3  15422  cxplt  15555  cxple  15556  rpcxple2  15557  rpcxplt2  15558  rpcxpsqrt  15561  rpabscxpbnd  15579  logbgt0b  15605  logbgcd1irr  15606  logbgcd1irraplemexp  15607  qdencn  16306  cvgcmp2nlemabs  16311  iooref1o  16313  trilpolemclim  16315  trilpolemisumle  16317  trilpolemeq1  16319  nconstwlpolemgt0  16343  taupi  16352