Theorem rpssre 12977

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

Syntax hints:   ⊆ wss 3940   class class class wbr 5138  ℝcr 11104  0cc0 11105   < clt 11244  ℝ⁺crp 12970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-in 3947  df-ss 3957  df-rp 12971

This theorem is referenced by:  rpre  12978  rpred  13012  rpexpcl  14042  rpexpmord  14129  01sqrexlem3  15187  fsumrpcl  15679  o1fsum  15755  divrcnv  15794  fprodrpcl  15896  rprisefaccl  15963  lebnumlem2  24798  bcthlem1  25162  bcthlem5  25166  aalioulem2  26175  efcvx  26291  pilem2  26294  pilem3  26295  dvrelog  26475  relogcn  26476  logcn  26485  advlog  26492  advlogexp  26493  loglesqrt  26597  rlimcnp  26801  rlimcnp3  26803  cxplim  26808  cxp2lim  26813  cxploglim  26814  divsqrtsumo1  26820  amgmlem  26826  logexprlim  27062  chto1ub  27313  chpo1ub  27317  chpo1ubb  27318  vmadivsum  27319  vmadivsumb  27320  rpvmasumlem  27324  dchrmusum2  27331  dchrvmasumlem2  27335  dchrvmasumiflem2  27339  dchrisum0fno1  27348  rpvmasum2  27349  dchrisum0lem1  27353  dchrisum0lem2a  27354  dchrisum0lem2  27355  dchrisum0  27357  dchrmusumlem  27359  rplogsum  27364  dirith2  27365  mudivsum  27367  mulogsumlem  27368  mulogsum  27369  mulog2sumlem2  27372  mulog2sumlem3  27373  log2sumbnd  27381  selberglem1  27382  selberglem2  27383  selberg2lem  27387  selberg2  27388  pntrmax  27401  pntrsumo1  27402  selbergr  27405  pntlem3  27446  pnt2  27450  rpdp2cl  32472  dp2lt10  32474  dp2lt  32475  dp2ltc  32477  xrge0iifhom  33372  omssubadd  33754  signsplypnf  34016  signsply0  34017  rpsqrtcn  34060  taupilem2  36659  taupi  36660  ptrecube  36944  heicant  36979  totbndbnd  37113  dvrelog2  41388  dvrelog3  41389  seff  43523  rpssxr  44642  ioorrnopnlem  45471  vonioolem1  45847  elbigolo1  47397  amgmwlem  48003  amgmlemALT  48004