Theorem rpssre 13152

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

This proof depends on syntax axioms:   ⊆ wss 3900   class class class wbr 5106  ℝcr 11223  0cc0 11224   < clt 11367  ℝ⁺crp 13144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-rp 13145

This theorem is used by:  rpre  13153  rpred  13188  rpexpcl  14247  rpexpmord  14335  01sqrexlem3  15437  fsumrpcl  15929  o1fsum  16006  divrcnv  16047  fprodrpcl  16149  rprisefaccl  16216  lebnumlem2  25310  bcthlem1  25672  bcthlem5  25676  aalioulem2  26687  efcvx  26803  pilem2  26806  pilem3  26807  dvrelog  26992  relogcn  26993  logcn  27002  advlog  27009  advlogexp  27010  loglesqrt  27116  rlimcnp  27320  rlimcnp3  27322  cxplim  27326  cxp2lim  27331  cxploglim  27332  divsqrtsumo1  27338  amgmlem  27344  logexprlim  27579  chto1ub  27830  chpo1ub  27834  chpo1ubb  27835  vmadivsum  27836  vmadivsumb  27837  rpvmasumlem  27841  dchrmusum2  27848  dchrvmasumlem2  27852  dchrvmasumiflem2  27856  dchrisum0fno1  27865  rpvmasum2  27866  dchrisum0lem1  27870  dchrisum0lem2a  27871  dchrisum0lem2  27872  dchrisum0  27874  dchrmusumlem  27876  rplogsum  27881  dirith2  27882  mudivsum  27884  mulogsumlem  27885  mulogsum  27886  mulog2sumlem2  27889  mulog2sumlem3  27890  log2sumbnd  27898  selberglem1  27899  selberglem2  27900  selberg2lem  27904  selberg2  27905  pntrmax  27918  pntrsumo1  27919  selbergr  27922  pntlem3  27963  pnt2  27967  rpdp2cl  33515  dp2lt10  33517  dp2lt  33518  dp2ltc  33520  xrge0iifhom  34636  signsplypnf  35246  signsply0  35247  rpsqrtcn  35289  taupilem2  38434  taupi  38435  ptrecube  38729  heicant  38764  totbndbnd  38914  dvrelog2  43305  dvrelog3  43306  rpsscn  43547  seff  45483  rpex  46561  rpssxr  46693  ioorrnopnlem  47517  vonioolem1  47893  lamberte  48141  elbigolo1  49872  amgmwlem  51265  amgmlemALT  51266