Theorem rpssre 12981

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

Syntax hints:   ⊆ wss 3949   class class class wbr 5149  ℝcr 11109  0cc0 11110   < clt 11248  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-rp 12975

This theorem is referenced by:  rpre  12982  rpred  13016  rpexpcl  14046  rpexpmord  14133  01sqrexlem3  15191  fsumrpcl  15683  o1fsum  15759  divrcnv  15798  fprodrpcl  15900  rprisefaccl  15967  lebnumlem2  24478  bcthlem1  24841  bcthlem5  24845  aalioulem2  25846  efcvx  25961  pilem2  25964  pilem3  25965  dvrelog  26145  relogcn  26146  logcn  26155  advlog  26162  advlogexp  26163  loglesqrt  26266  rlimcnp  26470  rlimcnp3  26472  cxplim  26476  cxp2lim  26481  cxploglim  26482  divsqrtsumo1  26488  amgmlem  26494  logexprlim  26728  chto1ub  26979  chpo1ub  26983  chpo1ubb  26984  vmadivsum  26985  vmadivsumb  26986  rpvmasumlem  26990  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumiflem2  27005  dchrisum0fno1  27014  rpvmasum2  27015  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0  27023  dchrmusumlem  27025  rplogsum  27030  dirith2  27031  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem2  27038  mulog2sumlem3  27039  log2sumbnd  27047  selberglem1  27048  selberglem2  27049  selberg2lem  27053  selberg2  27054  pntrmax  27067  pntrsumo1  27068  selbergr  27071  pntlem3  27112  pnt2  27116  rpdp2cl  32079  dp2lt10  32081  dp2lt  32082  dp2ltc  32084  xrge0iifhom  32948  omssubadd  33330  signsplypnf  33592  signsply0  33593  rpsqrtcn  33636  taupilem2  36251  taupi  36252  ptrecube  36536  heicant  36571  totbndbnd  36705  dvrelog2  40977  dvrelog3  40978  seff  43116  rpssxr  44239  ioorrnopnlem  45068  vonioolem1  45444  elbigolo1  47291  amgmwlem  47897  amgmlemALT  47898