Theorem rpssre 12927

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 12920	. 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥}
2	1	ssrab3 4036	1 ⊢ ℝ+ ⊆ ℝ

Syntax hints:   ⊆ wss 3903   class class class wbr 5100  ℝcr 11039  0cc0 11040   < clt 11180  ℝ⁺crp 12919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-rp 12920

This theorem is referenced by:  rpre  12928  rpred  12963  rpexpcl  14017  rpexpmord  14105  01sqrexlem3  15181  fsumrpcl  15674  o1fsum  15750  divrcnv  15789  fprodrpcl  15893  rprisefaccl  15960  lebnumlem2  24934  bcthlem1  25297  bcthlem5  25301  aalioulem2  26314  efcvx  26432  pilem2  26435  pilem3  26436  dvrelog  26619  relogcn  26620  logcn  26629  advlog  26636  advlogexp  26637  loglesqrt  26744  rlimcnp  26948  rlimcnp3  26950  cxplim  26955  cxp2lim  26960  cxploglim  26961  divsqrtsumo1  26967  amgmlem  26973  logexprlim  27209  chto1ub  27460  chpo1ub  27464  chpo1ubb  27465  vmadivsum  27466  vmadivsumb  27467  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumlem2  27482  dchrvmasumiflem2  27486  dchrisum0fno1  27495  rpvmasum2  27496  dchrisum0lem1  27500  dchrisum0lem2a  27501  dchrisum0lem2  27502  dchrisum0  27504  dchrmusumlem  27506  rplogsum  27511  dirith2  27512  mudivsum  27514  mulogsumlem  27515  mulogsum  27516  mulog2sumlem2  27519  mulog2sumlem3  27520  log2sumbnd  27528  selberglem1  27529  selberglem2  27530  selberg2lem  27534  selberg2  27535  pntrmax  27548  pntrsumo1  27549  selbergr  27552  pntlem3  27593  pnt2  27597  rpdp2cl  32980  dp2lt10  32982  dp2lt  32983  dp2ltc  32985  xrge0iifhom  34121  omssubadd  34484  signsplypnf  34734  signsply0  34735  rpsqrtcn  34777  taupilem2  37604  taupi  37605  ptrecube  37900  heicant  37935  totbndbnd  38069  dvrelog2  42463  dvrelog3  42464  rpsscn  42698  seff  44694  rpex  45734  rpssxr  45867  ioorrnopnlem  46691  vonioolem1  47067  lamberte  47277  elbigolo1  48946  amgmwlem  50190  amgmlemALT  50191