Theorem rpssre 12917

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

Syntax hints:   ⊆ wss 3902   class class class wbr 5099  ℝcr 11029  0cc0 11030   < clt 11170  ℝ⁺crp 12909

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-ss 3919  df-rp 12910

This theorem is referenced by:  rpre  12918  rpred  12953  rpexpcl  14007  rpexpmord  14095  01sqrexlem3  15171  fsumrpcl  15664  o1fsum  15740  divrcnv  15779  fprodrpcl  15883  rprisefaccl  15950  lebnumlem2  24921  bcthlem1  25284  bcthlem5  25288  aalioulem2  26301  efcvx  26419  pilem2  26422  pilem3  26423  dvrelog  26606  relogcn  26607  logcn  26616  advlog  26623  advlogexp  26624  loglesqrt  26731  rlimcnp  26935  rlimcnp3  26937  cxplim  26942  cxp2lim  26947  cxploglim  26948  divsqrtsumo1  26954  amgmlem  26960  logexprlim  27196  chto1ub  27447  chpo1ub  27451  chpo1ubb  27452  vmadivsum  27453  vmadivsumb  27454  rpvmasumlem  27458  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumiflem2  27473  dchrisum0fno1  27482  rpvmasum2  27483  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0  27491  dchrmusumlem  27493  rplogsum  27498  dirith2  27499  mudivsum  27501  mulogsumlem  27502  mulogsum  27503  mulog2sumlem2  27506  mulog2sumlem3  27507  log2sumbnd  27515  selberglem1  27516  selberglem2  27517  selberg2lem  27521  selberg2  27522  pntrmax  27535  pntrsumo1  27536  selbergr  27539  pntlem3  27580  pnt2  27584  rpdp2cl  32965  dp2lt10  32967  dp2lt  32968  dp2ltc  32970  xrge0iifhom  34096  omssubadd  34459  signsplypnf  34709  signsply0  34710  rpsqrtcn  34752  taupilem2  37529  taupi  37530  ptrecube  37823  heicant  37858  totbndbnd  37992  dvrelog2  42386  dvrelog3  42387  rpsscn  42621  seff  44617  rpex  45658  rpssxr  45791  ioorrnopnlem  46615  vonioolem1  46991  lamberte  47201  elbigolo1  48870  amgmwlem  50114  amgmlemALT  50115