Theorem rpssre 13083

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

This proof depends on syntax axioms:   ⊆ wss 3899   class class class wbr 5103  ℝcr 11156  0cc0 11157   < clt 11300  ℝ⁺crp 13075

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3916  df-rp 13076

This theorem is used by:  rpre  13084  rpred  13119  rpexpcl  14177  rpexpmord  14265  01sqrexlem3  15364  fsumrpcl  15856  o1fsum  15933  divrcnv  15974  fprodrpcl  16076  rprisefaccl  16143  lebnumlem2  25230  bcthlem1  25592  bcthlem5  25596  aalioulem2  26609  efcvx  26725  pilem2  26728  pilem3  26729  dvrelog  26914  relogcn  26915  logcn  26924  advlog  26931  advlogexp  26932  loglesqrt  27038  rlimcnp  27242  rlimcnp3  27244  cxplim  27248  cxp2lim  27253  cxploglim  27254  divsqrtsumo1  27260  amgmlem  27266  logexprlim  27501  chto1ub  27752  chpo1ub  27756  chpo1ubb  27757  vmadivsum  27758  vmadivsumb  27759  rpvmasumlem  27763  dchrmusum2  27770  dchrvmasumlem2  27774  dchrvmasumiflem2  27778  dchrisum0fno1  27787  rpvmasum2  27788  dchrisum0lem1  27792  dchrisum0lem2a  27793  dchrisum0lem2  27794  dchrisum0  27796  dchrmusumlem  27798  rplogsum  27803  dirith2  27804  mudivsum  27806  mulogsumlem  27807  mulogsum  27808  mulog2sumlem2  27811  mulog2sumlem3  27812  log2sumbnd  27820  selberglem1  27821  selberglem2  27822  selberg2lem  27826  selberg2  27827  pntrmax  27840  pntrsumo1  27841  selbergr  27844  pntlem3  27885  pnt2  27889  rpdp2cl  33367  dp2lt10  33369  dp2lt  33370  dp2ltc  33372  xrge0iifhom  34488  omssubadd  34852  signsplypnf  35099  signsply0  35100  rpsqrtcn  35142  taupilem2  38157  taupi  38158  ptrecube  38452  heicant  38487  totbndbnd  38637  dvrelog2  43028  dvrelog3  43029  rpsscn  43272  seff  45231  rpex  46274  rpssxr  46406  ioorrnopnlem  47230  vonioolem1  47606  lamberte  47854  elbigolo1  49585  amgmwlem  50903  amgmlemALT  50904