Theorem rpssre 13128

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

This proof depends on syntax axioms:   ⊆ wss 3899   class class class wbr 5103  ℝcr 11199  0cc0 11200   < clt 11343  ℝ⁺crp 13120

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3916  df-rp 13121

This theorem is used by:  rpre  13129  rpred  13164  rpexpcl  14223  rpexpmord  14311  01sqrexlem3  15411  fsumrpcl  15903  o1fsum  15980  divrcnv  16021  fprodrpcl  16123  rprisefaccl  16190  lebnumlem2  25283  bcthlem1  25645  bcthlem5  25649  aalioulem2  26660  efcvx  26776  pilem2  26779  pilem3  26780  dvrelog  26965  relogcn  26966  logcn  26975  advlog  26982  advlogexp  26983  loglesqrt  27089  rlimcnp  27293  rlimcnp3  27295  cxplim  27299  cxp2lim  27304  cxploglim  27305  divsqrtsumo1  27311  amgmlem  27317  logexprlim  27552  chto1ub  27803  chpo1ub  27807  chpo1ubb  27808  vmadivsum  27809  vmadivsumb  27810  rpvmasumlem  27814  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumiflem2  27829  dchrisum0fno1  27838  rpvmasum2  27839  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  dchrisum0  27847  dchrmusumlem  27849  rplogsum  27854  dirith2  27855  mudivsum  27857  mulogsumlem  27858  mulogsum  27859  mulog2sumlem2  27862  mulog2sumlem3  27863  log2sumbnd  27871  selberglem1  27872  selberglem2  27873  selberg2lem  27877  selberg2  27878  pntrmax  27891  pntrsumo1  27892  selbergr  27895  pntlem3  27936  pnt2  27940  rpdp2cl  33448  dp2lt10  33450  dp2lt  33451  dp2ltc  33453  xrge0iifhom  34569  omssubadd  34932  signsplypnf  35179  signsply0  35180  rpsqrtcn  35222  taupilem2  38243  taupi  38244  ptrecube  38538  heicant  38573  totbndbnd  38723  dvrelog2  43114  dvrelog3  43115  rpsscn  43356  seff  45292  rpex  46357  rpssxr  46489  ioorrnopnlem  47313  vonioolem1  47689  lamberte  47937  elbigolo1  49668  amgmwlem  50986  amgmlemALT  50987