Theorem rpssre 13052

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

This proof depends on syntax axioms:   ⊆ wss 3902   class class class wbr 5107  ℝcr 11126  0cc0 11127   < clt 11270  ℝ⁺crp 13044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-ss 3919  df-rp 13045

This theorem is used by:  rpre  13053  rpred  13088  rpexpcl  14146  rpexpmord  14234  01sqrexlem3  15333  fsumrpcl  15825  o1fsum  15902  divrcnv  15943  fprodrpcl  16047  rprisefaccl  16114  lebnumlem2  25191  bcthlem1  25553  bcthlem5  25557  aalioulem2  26566  efcvx  26682  pilem2  26685  pilem3  26686  dvrelog  26872  relogcn  26873  logcn  26882  advlog  26889  advlogexp  26890  loglesqrt  26996  rlimcnp  27200  rlimcnp3  27202  cxplim  27206  cxp2lim  27211  cxploglim  27212  divsqrtsumo1  27218  amgmlem  27224  logexprlim  27459  chto1ub  27710  chpo1ub  27714  chpo1ubb  27715  vmadivsum  27716  vmadivsumb  27717  rpvmasumlem  27721  dchrmusum2  27728  dchrvmasumlem2  27732  dchrvmasumiflem2  27736  dchrisum0fno1  27745  rpvmasum2  27746  dchrisum0lem1  27750  dchrisum0lem2a  27751  dchrisum0lem2  27752  dchrisum0  27754  dchrmusumlem  27756  rplogsum  27761  dirith2  27762  mudivsum  27764  mulogsumlem  27765  mulogsum  27766  mulog2sumlem2  27769  mulog2sumlem3  27770  log2sumbnd  27778  selberglem1  27779  selberglem2  27780  selberg2lem  27784  selberg2  27785  pntrmax  27798  pntrsumo1  27799  selbergr  27802  pntlem3  27843  pnt2  27847  rpdp2cl  33314  dp2lt10  33316  dp2lt  33317  dp2ltc  33319  xrge0iifhom  34434  omssubadd  34798  signsplypnf  35045  signsply0  35046  rpsqrtcn  35088  taupilem2  38061  taupi  38062  ptrecube  38356  heicant  38391  totbndbnd  38526  dvrelog2  42917  dvrelog3  42918  rpsscn  43161  seff  45120  rpex  46163  rpssxr  46295  ioorrnopnlem  47119  vonioolem1  47495  lamberte  47743  elbigolo1  49474  amgmwlem  50807  amgmlemALT  50808