Theorem rpssre 12945

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

Syntax hints:   ⊆ wss 3885   class class class wbr 5075  ℝcr 11032  0cc0 11033   < clt 11174  ℝ⁺crp 12937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-ss 3902  df-rp 12938

This theorem is referenced by:  rpre  12946  rpred  12981  rpexpcl  14037  rpexpmord  14125  01sqrexlem3  15201  fsumrpcl  15694  o1fsum  15771  divrcnv  15812  fprodrpcl  15916  rprisefaccl  15983  lebnumlem2  24951  bcthlem1  25313  bcthlem5  25317  aalioulem2  26321  efcvx  26436  pilem2  26439  pilem3  26440  dvrelog  26623  relogcn  26624  logcn  26633  advlog  26640  advlogexp  26641  loglesqrt  26747  rlimcnp  26951  rlimcnp3  26953  cxplim  26957  cxp2lim  26962  cxploglim  26963  divsqrtsumo1  26969  amgmlem  26975  logexprlim  27210  chto1ub  27461  chpo1ub  27465  chpo1ubb  27466  vmadivsum  27467  vmadivsumb  27468  rpvmasumlem  27472  dchrmusum2  27479  dchrvmasumlem2  27483  dchrvmasumiflem2  27487  dchrisum0fno1  27496  rpvmasum2  27497  dchrisum0lem1  27501  dchrisum0lem2a  27502  dchrisum0lem2  27503  dchrisum0  27505  dchrmusumlem  27507  rplogsum  27512  dirith2  27513  mudivsum  27515  mulogsumlem  27516  mulogsum  27517  mulog2sumlem2  27520  mulog2sumlem3  27521  log2sumbnd  27529  selberglem1  27530  selberglem2  27531  selberg2lem  27535  selberg2  27536  pntrmax  27549  pntrsumo1  27550  selbergr  27553  pntlem3  27594  pnt2  27598  rpdp2cl  32964  dp2lt10  32966  dp2lt  32967  dp2ltc  32969  xrge0iifhom  34133  omssubadd  34496  signsplypnf  34746  signsply0  34747  rpsqrtcn  34789  taupilem2  37697  taupi  37698  ptrecube  38002  heicant  38037  totbndbnd  38171  dvrelog2  42564  dvrelog3  42565  rpsscn  42791  seff  44768  rpex  45805  rpssxr  45937  ioorrnopnlem  46761  vonioolem1  47137  lamberte  47365  elbigolo1  49062  amgmwlem  50306  amgmlemALT  50307