Theorem rpssre 12950

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

Syntax hints:   ⊆ wss 3889   class class class wbr 5085  ℝcr 11037  0cc0 11038   < clt 11179  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-rp 12943

This theorem is referenced by:  rpre  12951  rpred  12986  rpexpcl  14042  rpexpmord  14130  01sqrexlem3  15206  fsumrpcl  15699  o1fsum  15776  divrcnv  15817  fprodrpcl  15921  rprisefaccl  15988  lebnumlem2  24929  bcthlem1  25291  bcthlem5  25295  aalioulem2  26299  efcvx  26414  pilem2  26417  pilem3  26418  dvrelog  26601  relogcn  26602  logcn  26611  advlog  26618  advlogexp  26619  loglesqrt  26725  rlimcnp  26929  rlimcnp3  26931  cxplim  26935  cxp2lim  26940  cxploglim  26941  divsqrtsumo1  26947  amgmlem  26953  logexprlim  27188  chto1ub  27439  chpo1ub  27443  chpo1ubb  27444  vmadivsum  27445  vmadivsumb  27446  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumiflem2  27465  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0  27483  dchrmusumlem  27485  rplogsum  27490  dirith2  27491  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  mulog2sumlem3  27499  log2sumbnd  27507  selberglem1  27508  selberglem2  27509  selberg2lem  27513  selberg2  27514  pntrmax  27527  pntrsumo1  27528  selbergr  27531  pntlem3  27572  pnt2  27576  rpdp2cl  32941  dp2lt10  32943  dp2lt  32944  dp2ltc  32946  xrge0iifhom  34081  omssubadd  34444  signsplypnf  34694  signsply0  34695  rpsqrtcn  34737  taupilem2  37636  taupi  37637  ptrecube  37941  heicant  37976  totbndbnd  38110  dvrelog2  42503  dvrelog3  42504  rpsscn  42731  seff  44736  rpex  45776  rpssxr  45908  ioorrnopnlem  46732  vonioolem1  47108  lamberte  47336  elbigolo1  49033  amgmwlem  50277  amgmlemALT  50278