Theorem rpssre 12384

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

Syntax hints:   ⊆ wss 3881   class class class wbr 5030  ℝcr 10525  0cc0 10526   < clt 10664  ℝ⁺crp 12377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-rp 12378

This theorem is referenced by:  rpre  12385  rpred  12419  rpexpcl  13444  rpexpmord  13528  sqrlem3  14596  fsumrpcl  15086  o1fsum  15160  divrcnv  15199  fprodrpcl  15302  rprisefaccl  15369  lebnumlem2  23567  bcthlem1  23928  bcthlem5  23932  aalioulem2  24929  efcvx  25044  pilem2  25047  pilem3  25048  dvrelog  25228  relogcn  25229  logcn  25238  advlog  25245  advlogexp  25246  loglesqrt  25347  rlimcnp  25551  rlimcnp3  25553  cxplim  25557  cxp2lim  25562  cxploglim  25563  divsqrtsumo1  25569  amgmlem  25575  logexprlim  25809  chto1ub  26060  chpo1ub  26064  chpo1ubb  26065  vmadivsum  26066  vmadivsumb  26067  rpvmasumlem  26071  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumiflem2  26086  dchrisum0fno1  26095  rpvmasum2  26096  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0  26104  dchrmusumlem  26106  rplogsum  26111  dirith2  26112  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem2  26119  mulog2sumlem3  26120  log2sumbnd  26128  selberglem1  26129  selberglem2  26130  selberg2lem  26134  selberg2  26135  pntrmax  26148  pntrsumo1  26149  selbergr  26152  pntlem3  26193  pnt2  26197  rpdp2cl  30584  dp2lt10  30586  dp2lt  30587  dp2ltc  30589  xrge0iifhom  31290  omssubadd  31668  signsplypnf  31930  signsply0  31931  rpsqrtcn  31974  taupilem2  34736  taupi  34737  ptrecube  35057  heicant  35092  totbndbnd  35227  seff  41013  rpssxr  42120  ioorrnopnlem  42946  vonioolem1  43319  elbigolo1  44971  amgmwlem  45330  amgmlemALT  45331