Theorem rpssre 12898

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

Syntax hints:   ⊆ wss 3897   class class class wbr 5089  ℝcr 11005  0cc0 11006   < clt 11146  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-rp 12891

This theorem is referenced by:  rpre  12899  rpred  12934  rpexpcl  13987  rpexpmord  14075  01sqrexlem3  15151  fsumrpcl  15644  o1fsum  15720  divrcnv  15759  fprodrpcl  15863  rprisefaccl  15930  lebnumlem2  24888  bcthlem1  25251  bcthlem5  25255  aalioulem2  26268  efcvx  26386  pilem2  26389  pilem3  26390  dvrelog  26573  relogcn  26574  logcn  26583  advlog  26590  advlogexp  26591  loglesqrt  26698  rlimcnp  26902  rlimcnp3  26904  cxplim  26909  cxp2lim  26914  cxploglim  26915  divsqrtsumo1  26921  amgmlem  26927  logexprlim  27163  chto1ub  27414  chpo1ub  27418  chpo1ubb  27419  vmadivsum  27420  vmadivsumb  27421  rpvmasumlem  27425  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumiflem2  27440  dchrisum0fno1  27449  rpvmasum2  27450  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrisum0  27458  dchrmusumlem  27460  rplogsum  27465  dirith2  27466  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  mulog2sumlem2  27473  mulog2sumlem3  27474  log2sumbnd  27482  selberglem1  27483  selberglem2  27484  selberg2lem  27488  selberg2  27489  pntrmax  27502  pntrsumo1  27503  selbergr  27506  pntlem3  27547  pnt2  27551  rpdp2cl  32862  dp2lt10  32864  dp2lt  32865  dp2ltc  32867  xrge0iifhom  33950  omssubadd  34313  signsplypnf  34563  signsply0  34564  rpsqrtcn  34606  taupilem2  37366  taupi  37367  ptrecube  37659  heicant  37694  totbndbnd  37828  dvrelog2  42156  dvrelog3  42157  rpsscn  42391  seff  44401  rpex  45444  rpssxr  45577  ioorrnopnlem  46401  vonioolem1  46777  lamberte  46987  elbigolo1  48657  amgmwlem  49902  amgmlemALT  49903