Theorem rpssre 12737

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

Syntax hints:   ⊆ wss 3887   class class class wbr 5074  ℝcr 10870  0cc0 10871   < clt 11009  ℝ⁺crp 12730

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-rp 12731

This theorem is referenced by:  rpre  12738  rpred  12772  rpexpcl  13801  rpexpmord  13886  sqrlem3  14956  fsumrpcl  15449  o1fsum  15525  divrcnv  15564  fprodrpcl  15666  rprisefaccl  15733  lebnumlem2  24125  bcthlem1  24488  bcthlem5  24492  aalioulem2  25493  efcvx  25608  pilem2  25611  pilem3  25612  dvrelog  25792  relogcn  25793  logcn  25802  advlog  25809  advlogexp  25810  loglesqrt  25911  rlimcnp  26115  rlimcnp3  26117  cxplim  26121  cxp2lim  26126  cxploglim  26127  divsqrtsumo1  26133  amgmlem  26139  logexprlim  26373  chto1ub  26624  chpo1ub  26628  chpo1ubb  26629  vmadivsum  26630  vmadivsumb  26631  rpvmasumlem  26635  dchrmusum2  26642  dchrvmasumlem2  26646  dchrvmasumiflem2  26650  dchrisum0fno1  26659  rpvmasum2  26660  dchrisum0lem1  26664  dchrisum0lem2a  26665  dchrisum0lem2  26666  dchrisum0  26668  dchrmusumlem  26670  rplogsum  26675  dirith2  26676  mudivsum  26678  mulogsumlem  26679  mulogsum  26680  mulog2sumlem2  26683  mulog2sumlem3  26684  log2sumbnd  26692  selberglem1  26693  selberglem2  26694  selberg2lem  26698  selberg2  26699  pntrmax  26712  pntrsumo1  26713  selbergr  26716  pntlem3  26757  pnt2  26761  rpdp2cl  31156  dp2lt10  31158  dp2lt  31159  dp2ltc  31161  xrge0iifhom  31887  omssubadd  32267  signsplypnf  32529  signsply0  32530  rpsqrtcn  32573  taupilem2  35493  taupi  35494  ptrecube  35777  heicant  35812  totbndbnd  35947  dvrelog2  40072  dvrelog3  40073  seff  41927  rpssxr  43021  ioorrnopnlem  43845  vonioolem1  44218  elbigolo1  45903  amgmwlem  46506  amgmlemALT  46507