Theorem rpssre 13025

Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)

Assertion

Ref	Expression
rpssre	⊢ ℝ+ ⊆ ℝ

Proof of Theorem rpssre

Step	Hyp	Ref	Expression
1		df-rp 13018	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2	1	ssrab3 4064	1 ⊢ ℝ+ ⊆ ℝ

Syntax hints:   ⊆ wss 3933   class class class wbr 5125  ℝcr 11137  0cc0 11138   < clt 11278  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-ss 3950  df-rp 13018

This theorem is referenced by:  rpre  13026  rpred  13060  rpexpcl  14104  rpexpmord  14191  01sqrexlem3  15266  fsumrpcl  15756  o1fsum  15832  divrcnv  15871  fprodrpcl  15975  rprisefaccl  16042  lebnumlem2  24949  bcthlem1  25313  bcthlem5  25317  aalioulem2  26330  efcvx  26448  pilem2  26451  pilem3  26452  dvrelog  26634  relogcn  26635  logcn  26644  advlog  26651  advlogexp  26652  loglesqrt  26759  rlimcnp  26963  rlimcnp3  26965  cxplim  26970  cxp2lim  26975  cxploglim  26976  divsqrtsumo1  26982  amgmlem  26988  logexprlim  27224  chto1ub  27475  chpo1ub  27479  chpo1ubb  27480  vmadivsum  27481  vmadivsumb  27482  rpvmasumlem  27486  dchrmusum2  27493  dchrvmasumlem2  27497  dchrvmasumiflem2  27501  dchrisum0fno1  27510  rpvmasum2  27511  dchrisum0lem1  27515  dchrisum0lem2a  27516  dchrisum0lem2  27517  dchrisum0  27519  dchrmusumlem  27521  rplogsum  27526  dirith2  27527  mudivsum  27529  mulogsumlem  27530  mulogsum  27531  mulog2sumlem2  27534  mulog2sumlem3  27535  log2sumbnd  27543  selberglem1  27544  selberglem2  27545  selberg2lem  27549  selberg2  27550  pntrmax  27563  pntrsumo1  27564  selbergr  27567  pntlem3  27608  pnt2  27612  rpdp2cl  32811  dp2lt10  32813  dp2lt  32814  dp2ltc  32816  xrge0iifhom  33877  omssubadd  34243  signsplypnf  34506  signsply0  34507  rpsqrtcn  34549  taupilem2  37264  taupi  37265  ptrecube  37568  heicant  37603  totbndbnd  37737  dvrelog2  42006  dvrelog3  42007  rpsscn  42278  seff  44273  rpex  45302  rpssxr  45436  ioorrnopnlem  46264  vonioolem1  46640  elbigolo1  48424  amgmwlem  49317  amgmlemALT  49318