Theorem rpssre 12491

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

Syntax hints:   ⊆ wss 3853   class class class wbr 5040  ℝcr 10626  0cc0 10627   < clt 10765  ℝ⁺crp 12484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402  df-in 3860  df-ss 3870  df-rp 12485

This theorem is referenced by:  rpre  12492  rpred  12526  rpexpcl  13552  rpexpmord  13636  sqrlem3  14706  fsumrpcl  15199  o1fsum  15273  divrcnv  15312  fprodrpcl  15414  rprisefaccl  15481  lebnumlem2  23726  bcthlem1  24088  bcthlem5  24092  aalioulem2  25093  efcvx  25208  pilem2  25211  pilem3  25212  dvrelog  25392  relogcn  25393  logcn  25402  advlog  25409  advlogexp  25410  loglesqrt  25511  rlimcnp  25715  rlimcnp3  25717  cxplim  25721  cxp2lim  25726  cxploglim  25727  divsqrtsumo1  25733  amgmlem  25739  logexprlim  25973  chto1ub  26224  chpo1ub  26228  chpo1ubb  26229  vmadivsum  26230  vmadivsumb  26231  rpvmasumlem  26235  dchrmusum2  26242  dchrvmasumlem2  26246  dchrvmasumiflem2  26250  dchrisum0fno1  26259  rpvmasum2  26260  dchrisum0lem1  26264  dchrisum0lem2a  26265  dchrisum0lem2  26266  dchrisum0  26268  dchrmusumlem  26270  rplogsum  26275  dirith2  26276  mudivsum  26278  mulogsumlem  26279  mulogsum  26280  mulog2sumlem2  26283  mulog2sumlem3  26284  log2sumbnd  26292  selberglem1  26293  selberglem2  26294  selberg2lem  26298  selberg2  26299  pntrmax  26312  pntrsumo1  26313  selbergr  26316  pntlem3  26357  pnt2  26361  rpdp2cl  30743  dp2lt10  30745  dp2lt  30746  dp2ltc  30748  xrge0iifhom  31471  omssubadd  31849  signsplypnf  32111  signsply0  32112  rpsqrtcn  32155  taupilem2  35145  taupi  35146  ptrecube  35432  heicant  35467  totbndbnd  35602  dvrelog2  39723  dvrelog3  39724  seff  41505  rpssxr  42601  ioorrnopnlem  43427  vonioolem1  43800  elbigolo1  45484  amgmwlem  46006  amgmlemALT  46007