Theorem rpssre 13040

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

Syntax hints:   ⊆ wss 3963   class class class wbr 5148  ℝcr 11152  0cc0 11153   < clt 11293  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-rp 13033

This theorem is referenced by:  rpre  13041  rpred  13075  rpexpcl  14118  rpexpmord  14205  01sqrexlem3  15280  fsumrpcl  15770  o1fsum  15846  divrcnv  15885  fprodrpcl  15989  rprisefaccl  16056  lebnumlem2  25008  bcthlem1  25372  bcthlem5  25376  aalioulem2  26390  efcvx  26508  pilem2  26511  pilem3  26512  dvrelog  26694  relogcn  26695  logcn  26704  advlog  26711  advlogexp  26712  loglesqrt  26819  rlimcnp  27023  rlimcnp3  27025  cxplim  27030  cxp2lim  27035  cxploglim  27036  divsqrtsumo1  27042  amgmlem  27048  logexprlim  27284  chto1ub  27535  chpo1ub  27539  chpo1ubb  27540  vmadivsum  27541  vmadivsumb  27542  rpvmasumlem  27546  dchrmusum2  27553  dchrvmasumlem2  27557  dchrvmasumiflem2  27561  dchrisum0fno1  27570  rpvmasum2  27571  dchrisum0lem1  27575  dchrisum0lem2a  27576  dchrisum0lem2  27577  dchrisum0  27579  dchrmusumlem  27581  rplogsum  27586  dirith2  27587  mudivsum  27589  mulogsumlem  27590  mulogsum  27591  mulog2sumlem2  27594  mulog2sumlem3  27595  log2sumbnd  27603  selberglem1  27604  selberglem2  27605  selberg2lem  27609  selberg2  27610  pntrmax  27623  pntrsumo1  27624  selbergr  27627  pntlem3  27668  pnt2  27672  rpdp2cl  32849  dp2lt10  32851  dp2lt  32852  dp2ltc  32854  xrge0iifhom  33898  omssubadd  34282  signsplypnf  34544  signsply0  34545  rpsqrtcn  34587  taupilem2  37305  taupi  37306  ptrecube  37607  heicant  37642  totbndbnd  37776  dvrelog2  42046  dvrelog3  42047  rpsscn  42312  seff  44305  rpex  45296  rpssxr  45431  ioorrnopnlem  46260  vonioolem1  46636  elbigolo1  48407  amgmwlem  49033  amgmlemALT  49034