Theorem rpssre 12915

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

Syntax hints:   ⊆ wss 3900   class class class wbr 5097  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12907

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-ss 3917  df-rp 12908

This theorem is referenced by:  rpre  12916  rpred  12951  rpexpcl  14005  rpexpmord  14093  01sqrexlem3  15169  fsumrpcl  15662  o1fsum  15738  divrcnv  15777  fprodrpcl  15881  rprisefaccl  15948  lebnumlem2  24919  bcthlem1  25282  bcthlem5  25286  aalioulem2  26299  efcvx  26417  pilem2  26420  pilem3  26421  dvrelog  26604  relogcn  26605  logcn  26614  advlog  26621  advlogexp  26622  loglesqrt  26729  rlimcnp  26933  rlimcnp3  26935  cxplim  26940  cxp2lim  26945  cxploglim  26946  divsqrtsumo1  26952  amgmlem  26958  logexprlim  27194  chto1ub  27445  chpo1ub  27449  chpo1ubb  27450  vmadivsum  27451  vmadivsumb  27452  rpvmasumlem  27456  dchrmusum2  27463  dchrvmasumlem2  27467  dchrvmasumiflem2  27471  dchrisum0fno1  27480  rpvmasum2  27481  dchrisum0lem1  27485  dchrisum0lem2a  27486  dchrisum0lem2  27487  dchrisum0  27489  dchrmusumlem  27491  rplogsum  27496  dirith2  27497  mudivsum  27499  mulogsumlem  27500  mulogsum  27501  mulog2sumlem2  27504  mulog2sumlem3  27505  log2sumbnd  27513  selberglem1  27514  selberglem2  27515  selberg2lem  27519  selberg2  27520  pntrmax  27533  pntrsumo1  27534  selbergr  27537  pntlem3  27578  pnt2  27582  rpdp2cl  32942  dp2lt10  32944  dp2lt  32945  dp2ltc  32947  xrge0iifhom  34073  omssubadd  34436  signsplypnf  34686  signsply0  34687  rpsqrtcn  34729  taupilem2  37496  taupi  37497  ptrecube  37790  heicant  37825  totbndbnd  37959  dvrelog2  42353  dvrelog3  42354  rpsscn  42591  seff  44587  rpex  45628  rpssxr  45761  ioorrnopnlem  46585  vonioolem1  46961  lamberte  47171  elbigolo1  48840  amgmwlem  50084  amgmlemALT  50085