Theorem rpssre 12931

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

Syntax hints:   ⊆ wss 3913   class class class wbr 5110  ℝcr 11059  0cc0 11060   < clt 11198  ℝ⁺crp 12924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-rp 12925

This theorem is referenced by:  rpre  12932  rpred  12966  rpexpcl  13996  rpexpmord  14083  01sqrexlem3  15141  fsumrpcl  15633  o1fsum  15709  divrcnv  15748  fprodrpcl  15850  rprisefaccl  15917  lebnumlem2  24362  bcthlem1  24725  bcthlem5  24729  aalioulem2  25730  efcvx  25845  pilem2  25848  pilem3  25849  dvrelog  26029  relogcn  26030  logcn  26039  advlog  26046  advlogexp  26047  loglesqrt  26148  rlimcnp  26352  rlimcnp3  26354  cxplim  26358  cxp2lim  26363  cxploglim  26364  divsqrtsumo1  26370  amgmlem  26376  logexprlim  26610  chto1ub  26861  chpo1ub  26865  chpo1ubb  26866  vmadivsum  26867  vmadivsumb  26868  rpvmasumlem  26872  dchrmusum2  26879  dchrvmasumlem2  26883  dchrvmasumiflem2  26887  dchrisum0fno1  26896  rpvmasum2  26897  dchrisum0lem1  26901  dchrisum0lem2a  26902  dchrisum0lem2  26903  dchrisum0  26905  dchrmusumlem  26907  rplogsum  26912  dirith2  26913  mudivsum  26915  mulogsumlem  26916  mulogsum  26917  mulog2sumlem2  26920  mulog2sumlem3  26921  log2sumbnd  26929  selberglem1  26930  selberglem2  26931  selberg2lem  26935  selberg2  26936  pntrmax  26949  pntrsumo1  26950  selbergr  26953  pntlem3  26994  pnt2  26998  rpdp2cl  31808  dp2lt10  31810  dp2lt  31811  dp2ltc  31813  xrge0iifhom  32607  omssubadd  32989  signsplypnf  33251  signsply0  33252  rpsqrtcn  33295  taupilem2  35866  taupi  35867  ptrecube  36151  heicant  36186  totbndbnd  36321  dvrelog2  40594  dvrelog3  40595  seff  42711  rpssxr  43836  ioorrnopnlem  44665  vonioolem1  45041  elbigolo1  46763  amgmwlem  47369  amgmlemALT  47370