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  32048  dp2lt10  32050  dp2lt  32051  dp2ltc  32053  xrge0iifhom  32917  omssubadd  33299  signsplypnf  33561  signsply0  33562  rpsqrtcn  33605  taupilem2  36203  taupi  36204  ptrecube  36488  heicant  36523  totbndbnd  36657  dvrelog2  40929  dvrelog3  40930  seff  43068  rpssxr  44191  ioorrnopnlem  45020  vonioolem1  45396  elbigolo1  47243  amgmwlem  47849  amgmlemALT  47850