Theorem rpssre 12935

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

Syntax hints:   ⊆ wss 3911   class class class wbr 5102  ℝcr 11043  0cc0 11044   < clt 11184  ℝ⁺crp 12927

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 3403  df-ss 3928  df-rp 12928

This theorem is referenced by:  rpre  12936  rpred  12971  rpexpcl  14021  rpexpmord  14109  01sqrexlem3  15186  fsumrpcl  15679  o1fsum  15755  divrcnv  15794  fprodrpcl  15898  rprisefaccl  15965  lebnumlem2  24894  bcthlem1  25257  bcthlem5  25261  aalioulem2  26274  efcvx  26392  pilem2  26395  pilem3  26396  dvrelog  26579  relogcn  26580  logcn  26589  advlog  26596  advlogexp  26597  loglesqrt  26704  rlimcnp  26908  rlimcnp3  26910  cxplim  26915  cxp2lim  26920  cxploglim  26921  divsqrtsumo1  26927  amgmlem  26933  logexprlim  27169  chto1ub  27420  chpo1ub  27424  chpo1ubb  27425  vmadivsum  27426  vmadivsumb  27427  rpvmasumlem  27431  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumiflem2  27446  dchrisum0fno1  27455  rpvmasum2  27456  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  dchrisum0  27464  dchrmusumlem  27466  rplogsum  27471  dirith2  27472  mudivsum  27474  mulogsumlem  27475  mulogsum  27476  mulog2sumlem2  27479  mulog2sumlem3  27480  log2sumbnd  27488  selberglem1  27489  selberglem2  27490  selberg2lem  27494  selberg2  27495  pntrmax  27508  pntrsumo1  27509  selbergr  27512  pntlem3  27553  pnt2  27557  rpdp2cl  32852  dp2lt10  32854  dp2lt  32855  dp2ltc  32857  xrge0iifhom  33920  omssubadd  34284  signsplypnf  34534  signsply0  34535  rpsqrtcn  34577  taupilem2  37303  taupi  37304  ptrecube  37607  heicant  37642  totbndbnd  37776  dvrelog2  42045  dvrelog3  42046  rpsscn  42280  seff  44291  rpex  45335  rpssxr  45469  ioorrnopnlem  46295  vonioolem1  46671  lamberte  46882  elbigolo1  48539  amgmwlem  49784  amgmlemALT  49785