Theorem rpssre 12959

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

Syntax hints:   ⊆ wss 3914   class class class wbr 5107  ℝcr 11067  0cc0 11068   < clt 11208  ℝ⁺crp 12951

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 3406  df-ss 3931  df-rp 12952

This theorem is referenced by:  rpre  12960  rpred  12995  rpexpcl  14045  rpexpmord  14133  01sqrexlem3  15210  fsumrpcl  15703  o1fsum  15779  divrcnv  15818  fprodrpcl  15922  rprisefaccl  15989  lebnumlem2  24861  bcthlem1  25224  bcthlem5  25228  aalioulem2  26241  efcvx  26359  pilem2  26362  pilem3  26363  dvrelog  26546  relogcn  26547  logcn  26556  advlog  26563  advlogexp  26564  loglesqrt  26671  rlimcnp  26875  rlimcnp3  26877  cxplim  26882  cxp2lim  26887  cxploglim  26888  divsqrtsumo1  26894  amgmlem  26900  logexprlim  27136  chto1ub  27387  chpo1ub  27391  chpo1ubb  27392  vmadivsum  27393  vmadivsumb  27394  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumiflem2  27413  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0  27431  dchrmusumlem  27433  rplogsum  27438  dirith2  27439  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem2  27446  mulog2sumlem3  27447  log2sumbnd  27455  selberglem1  27456  selberglem2  27457  selberg2lem  27461  selberg2  27462  pntrmax  27475  pntrsumo1  27476  selbergr  27479  pntlem3  27520  pnt2  27524  rpdp2cl  32802  dp2lt10  32804  dp2lt  32805  dp2ltc  32807  xrge0iifhom  33927  omssubadd  34291  signsplypnf  34541  signsply0  34542  rpsqrtcn  34584  taupilem2  37310  taupi  37311  ptrecube  37614  heicant  37649  totbndbnd  37783  dvrelog2  42052  dvrelog3  42053  rpsscn  42287  seff  44298  rpex  45342  rpssxr  45476  ioorrnopnlem  46302  vonioolem1  46678  lamberte  46889  elbigolo1  48546  amgmwlem  49791  amgmlemALT  49792