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 4007	1 ⊢ ℝ+ ⊆ ℝ

This proof depends on syntax axioms:   ⊆ wss 3895   class class class wbr 5102  ℝ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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  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  38244  taupi  38245  ptrecube  38539  heicant  38574  totbndbnd  38724  dvrelog2  43115  dvrelog3  43116  rpsscn  43357  seff  45293  rpex  46358  rpssxr  46490  ioorrnopnlem  47314  vonioolem1  47690  lamberte  47938  elbigolo1  49669  amgmwlem  50987  amgmlemALT  50988