Theorem rpssre 12945

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

Syntax hints:   ⊆ wss 3890   class class class wbr 5086  ℝcr 11032  0cc0 11033   < clt 11174  ℝ⁺crp 12937

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-ss 3907  df-rp 12938

This theorem is referenced by:  rpre  12946  rpred  12981  rpexpcl  14037  rpexpmord  14125  01sqrexlem3  15201  fsumrpcl  15694  o1fsum  15771  divrcnv  15812  fprodrpcl  15916  rprisefaccl  15983  lebnumlem2  24943  bcthlem1  25305  bcthlem5  25309  aalioulem2  26314  efcvx  26431  pilem2  26434  pilem3  26435  dvrelog  26618  relogcn  26619  logcn  26628  advlog  26635  advlogexp  26636  loglesqrt  26742  rlimcnp  26946  rlimcnp3  26948  cxplim  26953  cxp2lim  26958  cxploglim  26959  divsqrtsumo1  26965  amgmlem  26971  logexprlim  27206  chto1ub  27457  chpo1ub  27461  chpo1ubb  27462  vmadivsum  27463  vmadivsumb  27464  rpvmasumlem  27468  dchrmusum2  27475  dchrvmasumlem2  27479  dchrvmasumiflem2  27483  dchrisum0fno1  27492  rpvmasum2  27493  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0  27501  dchrmusumlem  27503  rplogsum  27508  dirith2  27509  mudivsum  27511  mulogsumlem  27512  mulogsum  27513  mulog2sumlem2  27516  mulog2sumlem3  27517  log2sumbnd  27525  selberglem1  27526  selberglem2  27527  selberg2lem  27531  selberg2  27532  pntrmax  27545  pntrsumo1  27546  selbergr  27549  pntlem3  27590  pnt2  27594  rpdp2cl  32960  dp2lt10  32962  dp2lt  32963  dp2ltc  32965  xrge0iifhom  34101  omssubadd  34464  signsplypnf  34714  signsply0  34715  rpsqrtcn  34757  taupilem2  37656  taupi  37657  ptrecube  37961  heicant  37996  totbndbnd  38130  dvrelog2  42523  dvrelog3  42524  rpsscn  42751  seff  44760  rpex  45800  rpssxr  45932  ioorrnopnlem  46756  vonioolem1  47132  lamberte  47354  elbigolo1  49051  amgmwlem  50295  amgmlemALT  50296