Theorem rpssre 13021

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

Syntax hints:   ⊆ wss 3931   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274  ℝ⁺crp 13013

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-ss 3948  df-rp 13014

This theorem is referenced by:  rpre  13022  rpred  13056  rpexpcl  14103  rpexpmord  14191  01sqrexlem3  15268  fsumrpcl  15758  o1fsum  15834  divrcnv  15873  fprodrpcl  15977  rprisefaccl  16044  lebnumlem2  24917  bcthlem1  25281  bcthlem5  25285  aalioulem2  26298  efcvx  26416  pilem2  26419  pilem3  26420  dvrelog  26603  relogcn  26604  logcn  26613  advlog  26620  advlogexp  26621  loglesqrt  26728  rlimcnp  26932  rlimcnp3  26934  cxplim  26939  cxp2lim  26944  cxploglim  26945  divsqrtsumo1  26951  amgmlem  26957  logexprlim  27193  chto1ub  27444  chpo1ub  27448  chpo1ubb  27449  vmadivsum  27450  vmadivsumb  27451  rpvmasumlem  27455  dchrmusum2  27462  dchrvmasumlem2  27466  dchrvmasumiflem2  27470  dchrisum0fno1  27479  rpvmasum2  27480  dchrisum0lem1  27484  dchrisum0lem2a  27485  dchrisum0lem2  27486  dchrisum0  27488  dchrmusumlem  27490  rplogsum  27495  dirith2  27496  mudivsum  27498  mulogsumlem  27499  mulogsum  27500  mulog2sumlem2  27503  mulog2sumlem3  27504  log2sumbnd  27512  selberglem1  27513  selberglem2  27514  selberg2lem  27518  selberg2  27519  pntrmax  27532  pntrsumo1  27533  selbergr  27536  pntlem3  27577  pnt2  27581  rpdp2cl  32861  dp2lt10  32863  dp2lt  32864  dp2ltc  32866  xrge0iifhom  33973  omssubadd  34337  signsplypnf  34587  signsply0  34588  rpsqrtcn  34630  taupilem2  37345  taupi  37346  ptrecube  37649  heicant  37684  totbndbnd  37818  dvrelog2  42082  dvrelog3  42083  rpsscn  42317  seff  44308  rpex  45353  rpssxr  45487  ioorrnopnlem  46313  vonioolem1  46689  lamberte  46900  elbigolo1  48517  amgmwlem  49646  amgmlemALT  49647