Theorem rpssre 12901

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

Syntax hints:   ⊆ wss 3903   class class class wbr 5092  ℝcr 11008  0cc0 11009   < clt 11149  ℝ⁺crp 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-ss 3920  df-rp 12894

This theorem is referenced by:  rpre  12902  rpred  12937  rpexpcl  13987  rpexpmord  14075  01sqrexlem3  15151  fsumrpcl  15644  o1fsum  15720  divrcnv  15759  fprodrpcl  15863  rprisefaccl  15930  lebnumlem2  24859  bcthlem1  25222  bcthlem5  25226  aalioulem2  26239  efcvx  26357  pilem2  26360  pilem3  26361  dvrelog  26544  relogcn  26545  logcn  26554  advlog  26561  advlogexp  26562  loglesqrt  26669  rlimcnp  26873  rlimcnp3  26875  cxplim  26880  cxp2lim  26885  cxploglim  26886  divsqrtsumo1  26892  amgmlem  26898  logexprlim  27134  chto1ub  27385  chpo1ub  27389  chpo1ubb  27390  vmadivsum  27391  vmadivsumb  27392  rpvmasumlem  27396  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumiflem2  27411  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  dchrisum0  27429  dchrmusumlem  27431  rplogsum  27436  dirith2  27437  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem2  27444  mulog2sumlem3  27445  log2sumbnd  27453  selberglem1  27454  selberglem2  27455  selberg2lem  27459  selberg2  27460  pntrmax  27473  pntrsumo1  27474  selbergr  27477  pntlem3  27518  pnt2  27522  rpdp2cl  32831  dp2lt10  32833  dp2lt  32834  dp2ltc  32836  xrge0iifhom  33920  omssubadd  34284  signsplypnf  34534  signsply0  34535  rpsqrtcn  34577  taupilem2  37316  taupi  37317  ptrecube  37620  heicant  37655  totbndbnd  37789  dvrelog2  42057  dvrelog3  42058  rpsscn  42292  seff  44302  rpex  45346  rpssxr  45479  ioorrnopnlem  46305  vonioolem1  46681  lamberte  46892  elbigolo1  48562  amgmwlem  49807  amgmlemALT  49808