Theorem rpssre 13030

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

This proof depends on syntax axioms:   ⊆ wss 3904   class class class wbr 5108  ℝcr 11105  0cc0 11106   < clt 11249  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-ss 3921  df-rp 13023

This theorem is used by:  rpre  13031  rpred  13066  rpexpcl  14123  rpexpmord  14211  01sqrexlem3  15302  fsumrpcl  15795  o1fsum  15872  divrcnv  15913  fprodrpcl  16017  rprisefaccl  16084  lebnumlem2  25132  bcthlem1  25494  bcthlem5  25498  aalioulem2  26507  efcvx  26623  pilem2  26626  pilem3  26627  dvrelog  26813  relogcn  26814  logcn  26823  advlog  26830  advlogexp  26831  loglesqrt  26937  rlimcnp  27141  rlimcnp3  27143  cxplim  27147  cxp2lim  27152  cxploglim  27153  divsqrtsumo1  27159  amgmlem  27165  logexprlim  27400  chto1ub  27651  chpo1ub  27655  chpo1ubb  27656  vmadivsum  27657  vmadivsumb  27658  rpvmasumlem  27662  dchrmusum2  27669  dchrvmasumlem2  27673  dchrvmasumiflem2  27677  dchrisum0fno1  27686  rpvmasum2  27687  dchrisum0lem1  27691  dchrisum0lem2a  27692  dchrisum0lem2  27693  dchrisum0  27695  dchrmusumlem  27697  rplogsum  27702  dirith2  27703  mudivsum  27705  mulogsumlem  27706  mulogsum  27707  mulog2sumlem2  27710  mulog2sumlem3  27711  log2sumbnd  27719  selberglem1  27720  selberglem2  27721  selberg2lem  27725  selberg2  27726  pntrmax  27739  pntrsumo1  27740  selbergr  27743  pntlem3  27784  pnt2  27788  rpdp2cl  33212  dp2lt10  33214  dp2lt  33215  dp2ltc  33217  xrge0iifhom  34336  omssubadd  34699  signsplypnf  34946  signsply0  34947  rpsqrtcn  34989  taupilem2  37994  taupi  37995  ptrecube  38299  heicant  38334  totbndbnd  38468  dvrelog2  42859  dvrelog3  42860  rpsscn  43088  seff  45047  rpex  46090  rpssxr  46222  ioorrnopnlem  47046  vonioolem1  47422  lamberte  47653  elbigolo1  49365  amgmwlem  50677  amgmlemALT  50678