Theorem rpssre 12399

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

Syntax hints:   ⊆ wss 3939   class class class wbr 5069  ℝcr 10539  0cc0 10540   < clt 10678  ℝ⁺crp 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-in 3946  df-ss 3955  df-rp 12393

This theorem is referenced by:  rpre  12400  rpred  12434  rpexpcl  13451  rpexpmord  13535  sqrlem3  14607  fsumrpcl  15097  o1fsum  15171  divrcnv  15210  fprodrpcl  15313  rprisefaccl  15380  lebnumlem2  23569  bcthlem1  23930  bcthlem5  23934  aalioulem2  24925  efcvx  25040  pilem2  25043  pilem3  25044  dvrelog  25223  relogcn  25224  logcn  25233  advlog  25240  advlogexp  25241  loglesqrt  25342  rlimcnp  25546  rlimcnp3  25548  cxplim  25552  cxp2lim  25557  cxploglim  25558  divsqrtsumo1  25564  amgmlem  25570  logexprlim  25804  chto1ub  26055  chpo1ub  26059  chpo1ubb  26060  vmadivsum  26061  vmadivsumb  26062  rpvmasumlem  26066  dchrmusum2  26073  dchrvmasumlem2  26077  dchrvmasumiflem2  26081  dchrisum0fno1  26090  rpvmasum2  26091  dchrisum0lem1  26095  dchrisum0lem2a  26096  dchrisum0lem2  26097  dchrisum0  26099  dchrmusumlem  26101  rplogsum  26106  dirith2  26107  mudivsum  26109  mulogsumlem  26110  mulogsum  26111  mulog2sumlem2  26114  mulog2sumlem3  26115  log2sumbnd  26123  selberglem1  26124  selberglem2  26125  selberg2lem  26129  selberg2  26130  pntrmax  26143  pntrsumo1  26144  selbergr  26147  pntlem3  26188  pnt2  26192  rpdp2cl  30562  dp2lt10  30564  dp2lt  30565  dp2ltc  30567  xrge0iifhom  31184  omssubadd  31562  signsplypnf  31824  signsply0  31825  rpsqrtcn  31868  taupilem2  34607  taupi  34608  ptrecube  34896  heicant  34931  totbndbnd  35071  seff  40647  rpssxr  41763  ioorrnopnlem  42596  vonioolem1  42969  elbigolo1  44624  amgmwlem  44910  amgmlemALT  44911