Theorem rpssre 13024

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

Syntax hints:   ⊆ wss 3931   class class class wbr 5123  ℝcr 11136  0cc0 11137   < clt 11277  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-ss 3948  df-rp 13017

This theorem is referenced by:  rpre  13025  rpred  13059  rpexpcl  14103  rpexpmord  14190  01sqrexlem3  15265  fsumrpcl  15755  o1fsum  15831  divrcnv  15870  fprodrpcl  15974  rprisefaccl  16041  lebnumlem2  24930  bcthlem1  25294  bcthlem5  25298  aalioulem2  26311  efcvx  26429  pilem2  26432  pilem3  26433  dvrelog  26615  relogcn  26616  logcn  26625  advlog  26632  advlogexp  26633  loglesqrt  26740  rlimcnp  26944  rlimcnp3  26946  cxplim  26951  cxp2lim  26956  cxploglim  26957  divsqrtsumo1  26963  amgmlem  26969  logexprlim  27205  chto1ub  27456  chpo1ub  27460  chpo1ubb  27461  vmadivsum  27462  vmadivsumb  27463  rpvmasumlem  27467  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumiflem2  27482  dchrisum0fno1  27491  rpvmasum2  27492  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrisum0  27500  dchrmusumlem  27502  rplogsum  27507  dirith2  27508  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem2  27515  mulog2sumlem3  27516  log2sumbnd  27524  selberglem1  27525  selberglem2  27526  selberg2lem  27530  selberg2  27531  pntrmax  27544  pntrsumo1  27545  selbergr  27548  pntlem3  27589  pnt2  27593  rpdp2cl  32804  dp2lt10  32806  dp2lt  32807  dp2ltc  32809  xrge0iifhom  33895  omssubadd  34261  signsplypnf  34524  signsply0  34525  rpsqrtcn  34567  taupilem2  37282  taupi  37283  ptrecube  37586  heicant  37621  totbndbnd  37755  dvrelog2  42024  dvrelog3  42025  rpsscn  42296  seff  44285  rpex  45314  rpssxr  45448  ioorrnopnlem  46276  vonioolem1  46652  elbigolo1  48436  amgmwlem  49329  amgmlemALT  49330