Theorem rpssre 13024

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

Syntax hints:   ⊆ wss 3911   class class class wbr 5111  ℝcr 11099  0cc0 11100   < clt 11243  ℝ⁺crp 13016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-ss 3928  df-rp 13017

This theorem is referenced by:  rpre  13025  rpred  13060  rpexpcl  14116  rpexpmord  14204  01sqrexlem3  15295  fsumrpcl  15788  o1fsum  15865  divrcnv  15906  fprodrpcl  16010  rprisefaccl  16077  lebnumlem2  25090  bcthlem1  25452  bcthlem5  25456  aalioulem2  26463  efcvx  26578  pilem2  26581  pilem3  26582  dvrelog  26768  relogcn  26769  logcn  26778  advlog  26785  advlogexp  26786  loglesqrt  26892  rlimcnp  27096  rlimcnp3  27098  cxplim  27102  cxp2lim  27107  cxploglim  27108  divsqrtsumo1  27114  amgmlem  27120  logexprlim  27355  chto1ub  27606  chpo1ub  27610  chpo1ubb  27611  vmadivsum  27612  vmadivsumb  27613  rpvmasumlem  27617  dchrmusum2  27624  dchrvmasumlem2  27628  dchrvmasumiflem2  27632  dchrisum0fno1  27641  rpvmasum2  27642  dchrisum0lem1  27646  dchrisum0lem2a  27647  dchrisum0lem2  27648  dchrisum0  27650  dchrmusumlem  27652  rplogsum  27657  dirith2  27658  mudivsum  27660  mulogsumlem  27661  mulogsum  27662  mulog2sumlem2  27665  mulog2sumlem3  27666  log2sumbnd  27674  selberglem1  27675  selberglem2  27676  selberg2lem  27680  selberg2  27681  pntrmax  27694  pntrsumo1  27695  selbergr  27698  pntlem3  27739  pnt2  27743  rpdp2cl  33142  dp2lt10  33144  dp2lt  33145  dp2ltc  33147  xrge0iifhom  34272  omssubadd  34635  signsplypnf  34882  signsply0  34883  rpsqrtcn  34925  taupilem2  37889  taupi  37890  ptrecube  38194  heicant  38229  totbndbnd  38363  dvrelog2  42756  dvrelog3  42757  rpsscn  42985  seff  44946  rpex  45989  rpssxr  46121  ioorrnopnlem  46945  vonioolem1  47321  lamberte  47549  elbigolo1  49257  amgmwlem  50511  amgmlemALT  50512