Theorem rpssre 13003

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

Syntax hints:   ⊆ wss 3906   class class class wbr 5102  ℝcr 11074  0cc0 11075   < clt 11218  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-ss 3923  df-rp 12996

This theorem is referenced by:  rpre  13004  rpred  13039  rpexpcl  14095  rpexpmord  14183  01sqrexlem3  15273  fsumrpcl  15766  o1fsum  15843  divrcnv  15884  fprodrpcl  15988  rprisefaccl  16055  lebnumlem2  25026  bcthlem1  25388  bcthlem5  25392  aalioulem2  26399  efcvx  26514  pilem2  26517  pilem3  26518  dvrelog  26704  relogcn  26705  logcn  26714  advlog  26721  advlogexp  26722  loglesqrt  26828  rlimcnp  27032  rlimcnp3  27034  cxplim  27038  cxp2lim  27043  cxploglim  27044  divsqrtsumo1  27050  amgmlem  27056  logexprlim  27291  chto1ub  27542  chpo1ub  27546  chpo1ubb  27547  vmadivsum  27548  vmadivsumb  27549  rpvmasumlem  27553  dchrmusum2  27560  dchrvmasumlem2  27564  dchrvmasumiflem2  27568  dchrisum0fno1  27577  rpvmasum2  27578  dchrisum0lem1  27582  dchrisum0lem2a  27583  dchrisum0lem2  27584  dchrisum0  27586  dchrmusumlem  27588  rplogsum  27593  dirith2  27594  mudivsum  27596  mulogsumlem  27597  mulogsum  27598  mulog2sumlem2  27601  mulog2sumlem3  27602  log2sumbnd  27610  selberglem1  27611  selberglem2  27612  selberg2lem  27616  selberg2  27617  pntrmax  27630  pntrsumo1  27631  selbergr  27634  pntlem3  27675  pnt2  27679  rpdp2cl  33061  dp2lt10  33063  dp2lt  33064  dp2ltc  33066  xrge0iifhom  34236  omssubadd  34599  signsplypnf  34846  signsply0  34847  rpsqrtcn  34889  taupilem2  37819  taupi  37820  ptrecube  38124  heicant  38159  totbndbnd  38293  dvrelog2  42686  dvrelog3  42687  rpsscn  42913  seff  44890  rpex  45927  rpssxr  46059  ioorrnopnlem  46883  vonioolem1  47259  lamberte  47487  elbigolo1  49184  amgmwlem  50428  amgmlemALT  50429