Theorem rpssre 11843

Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.)

Assertion

Ref	Expression
rpssre	|- RR+ C_ RR

Proof of Theorem rpssre

Step	Hyp	Ref	Expression
1		rpre 11839	. 2 |- ( x e. RR+ -> x e. RR )
2	1	ssriv 3607	1 |- RR+ C_ RR

Syntax hints:   C_ wss 3574   RRcr 9935   RR+crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-in 3581  df-ss 3588  df-rp 11833

This theorem is referenced by:  rpred  11872  rpexpcl  12879  sqrlem3  13985  fsumrpcl  14468  o1fsum  14545  divrcnv  14584  fprodrpcl  14686  rprisefaccl  14754  lebnumlem2  22761  bcthlem1  23121  bcthlem5  23125  aalioulem2  24088  efcvx  24203  pilem2  24206  pilem3  24207  dvrelog  24383  relogcn  24384  logcn  24393  advlog  24400  advlogexp  24401  loglesqrt  24499  rlimcnp  24692  rlimcnp3  24694  cxplim  24698  cxp2lim  24703  cxploglim  24704  divsqrtsumo1  24710  amgmlem  24716  logexprlim  24950  chto1ub  25165  chpo1ub  25169  chpo1ubb  25170  vmadivsum  25171  vmadivsumb  25172  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumiflem2  25191  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0  25209  dchrmusumlem  25211  rplogsum  25216  dirith2  25217  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem2  25224  mulog2sumlem3  25225  log2sumbnd  25233  selberglem1  25234  selberglem2  25235  selberg2lem  25239  selberg2  25240  pntrmax  25253  pntrsumo1  25254  selbergr  25257  pntlem3  25298  pnt2  25302  rpdp2cl  29589  dp2lt10  29591  dp2lt  29592  dp2ltc  29594  xrge0iifhom  29983  omssubadd  30362  signsplypnf  30627  signsply0  30628  rpsqrtcn  30671  taupilem2  33168  taupi  33169  ptrecube  33409  heicant  33444  totbndbnd  33588  rpexpmord  37513  seff  38508  rpssxr  39711  ioorrnopnlem  40524  vonioolem1  40894  elbigolo1  42351  amgmwlem  42548  amgmlemALT  42549