Theorem rpssre 13064

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

Syntax hints:   ⊆ wss 3976   class class class wbr 5166  ℝcr 11183  0cc0 11184   < clt 11324  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-rp 13058

This theorem is referenced by:  rpre  13065  rpred  13099  rpexpcl  14131  rpexpmord  14218  01sqrexlem3  15293  fsumrpcl  15785  o1fsum  15861  divrcnv  15900  fprodrpcl  16004  rprisefaccl  16071  lebnumlem2  25013  bcthlem1  25377  bcthlem5  25381  aalioulem2  26393  efcvx  26511  pilem2  26514  pilem3  26515  dvrelog  26697  relogcn  26698  logcn  26707  advlog  26714  advlogexp  26715  loglesqrt  26822  rlimcnp  27026  rlimcnp3  27028  cxplim  27033  cxp2lim  27038  cxploglim  27039  divsqrtsumo1  27045  amgmlem  27051  logexprlim  27287  chto1ub  27538  chpo1ub  27542  chpo1ubb  27543  vmadivsum  27544  vmadivsumb  27545  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumiflem2  27564  dchrisum0fno1  27573  rpvmasum2  27574  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0  27582  dchrmusumlem  27584  rplogsum  27589  dirith2  27590  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  mulog2sumlem2  27597  mulog2sumlem3  27598  log2sumbnd  27606  selberglem1  27607  selberglem2  27608  selberg2lem  27612  selberg2  27613  pntrmax  27626  pntrsumo1  27627  selbergr  27630  pntlem3  27671  pnt2  27675  rpdp2cl  32846  dp2lt10  32848  dp2lt  32849  dp2ltc  32851  xrge0iifhom  33883  omssubadd  34265  signsplypnf  34527  signsply0  34528  rpsqrtcn  34570  taupilem2  37288  taupi  37289  ptrecube  37580  heicant  37615  totbndbnd  37749  dvrelog2  42021  dvrelog3  42022  seff  44278  rpssxr  45396  ioorrnopnlem  46225  vonioolem1  46601  elbigolo1  48291  amgmwlem  48896  amgmlemALT  48897