Theorem rpssre 12666

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

Syntax hints:   ⊆ wss 3883   class class class wbr 5070  ℝcr 10801  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-rp 12660

This theorem is referenced by:  rpre  12667  rpred  12701  rpexpcl  13729  rpexpmord  13814  sqrlem3  14884  fsumrpcl  15377  o1fsum  15453  divrcnv  15492  fprodrpcl  15594  rprisefaccl  15661  lebnumlem2  24031  bcthlem1  24393  bcthlem5  24397  aalioulem2  25398  efcvx  25513  pilem2  25516  pilem3  25517  dvrelog  25697  relogcn  25698  logcn  25707  advlog  25714  advlogexp  25715  loglesqrt  25816  rlimcnp  26020  rlimcnp3  26022  cxplim  26026  cxp2lim  26031  cxploglim  26032  divsqrtsumo1  26038  amgmlem  26044  logexprlim  26278  chto1ub  26529  chpo1ub  26533  chpo1ubb  26534  vmadivsum  26535  vmadivsumb  26536  rpvmasumlem  26540  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumiflem2  26555  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0  26573  dchrmusumlem  26575  rplogsum  26580  dirith2  26581  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem2  26588  mulog2sumlem3  26589  log2sumbnd  26597  selberglem1  26598  selberglem2  26599  selberg2lem  26603  selberg2  26604  pntrmax  26617  pntrsumo1  26618  selbergr  26621  pntlem3  26662  pnt2  26666  rpdp2cl  31058  dp2lt10  31060  dp2lt  31061  dp2ltc  31063  xrge0iifhom  31789  omssubadd  32167  signsplypnf  32429  signsply0  32430  rpsqrtcn  32473  taupilem2  35420  taupi  35421  ptrecube  35704  heicant  35739  totbndbnd  35874  dvrelog2  40000  dvrelog3  40001  seff  41816  rpssxr  42911  ioorrnopnlem  43735  vonioolem1  44108  elbigolo1  45791  amgmwlem  46392  amgmlemALT  46393