Theorem rpssre 12390

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

Syntax hints:   ⊆ wss 3935   class class class wbr 5058  ℝcr 10530  0cc0 10531   < clt 10669  ℝ⁺crp 12383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-in 3942  df-ss 3951  df-rp 12384

This theorem is referenced by:  rpre  12391  rpred  12425  rpexpcl  13442  rpexpmord  13526  sqrlem3  14598  fsumrpcl  15088  o1fsum  15162  divrcnv  15201  fprodrpcl  15304  rprisefaccl  15371  lebnumlem2  23560  bcthlem1  23921  bcthlem5  23925  aalioulem2  24916  efcvx  25031  pilem2  25034  pilem3  25035  dvrelog  25214  relogcn  25215  logcn  25224  advlog  25231  advlogexp  25232  loglesqrt  25333  rlimcnp  25537  rlimcnp3  25539  cxplim  25543  cxp2lim  25548  cxploglim  25549  divsqrtsumo1  25555  amgmlem  25561  logexprlim  25795  chto1ub  26046  chpo1ub  26050  chpo1ubb  26051  vmadivsum  26052  vmadivsumb  26053  rpvmasumlem  26057  dchrmusum2  26064  dchrvmasumlem2  26068  dchrvmasumiflem2  26072  dchrisum0fno1  26081  rpvmasum2  26082  dchrisum0lem1  26086  dchrisum0lem2a  26087  dchrisum0lem2  26088  dchrisum0  26090  dchrmusumlem  26092  rplogsum  26097  dirith2  26098  mudivsum  26100  mulogsumlem  26101  mulogsum  26102  mulog2sumlem2  26105  mulog2sumlem3  26106  log2sumbnd  26114  selberglem1  26115  selberglem2  26116  selberg2lem  26120  selberg2  26121  pntrmax  26134  pntrsumo1  26135  selbergr  26138  pntlem3  26179  pnt2  26183  rpdp2cl  30553  dp2lt10  30555  dp2lt  30556  dp2ltc  30558  xrge0iifhom  31175  omssubadd  31553  signsplypnf  31815  signsply0  31816  rpsqrtcn  31859  taupilem2  34597  taupi  34598  ptrecube  34886  heicant  34921  totbndbnd  35061  seff  40634  rpssxr  41750  ioorrnopnlem  42583  vonioolem1  42956  elbigolo1  44611  amgmwlem  44897  amgmlemALT  44898