Theorem rpssre 12144

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

Syntax hints:   ⊆ wss 3792   class class class wbr 4886  ℝcr 10271  0cc0 10272   < clt 10411  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-in 3799  df-ss 3806  df-rp 12138

This theorem is referenced by:  rpre  12145  rpred  12181  rpexpcl  13197  sqrlem3  14392  fsumrpcl  14875  o1fsum  14949  divrcnv  14988  fprodrpcl  15089  rprisefaccl  15156  lebnumlem2  23169  bcthlem1  23530  bcthlem5  23534  aalioulem2  24525  efcvx  24640  pilem2  24643  pilem3  24644  pilem3OLD  24645  dvrelog  24820  relogcn  24821  logcn  24830  advlog  24837  advlogexp  24838  loglesqrt  24939  rlimcnp  25144  rlimcnp3  25146  cxplim  25150  cxp2lim  25155  cxploglim  25156  divsqrtsumo1  25162  amgmlem  25168  logexprlim  25402  chto1ub  25617  chpo1ub  25621  chpo1ubb  25622  vmadivsum  25623  vmadivsumb  25624  rpvmasumlem  25628  dchrmusum2  25635  dchrvmasumlem2  25639  dchrvmasumiflem2  25643  dchrisum0fno1  25652  rpvmasum2  25653  dchrisum0lem1  25657  dchrisum0lem2a  25658  dchrisum0lem2  25659  dchrisum0  25661  dchrmusumlem  25663  rplogsum  25668  dirith2  25669  mudivsum  25671  mulogsumlem  25672  mulogsum  25673  mulog2sumlem2  25676  mulog2sumlem3  25677  log2sumbnd  25685  selberglem1  25686  selberglem2  25687  selberg2lem  25691  selberg2  25692  pntrmax  25705  pntrsumo1  25706  selbergr  25709  pntlem3  25750  pnt2  25754  rpdp2cl  30152  dp2lt10  30154  dp2lt  30155  dp2ltc  30157  xrge0iifhom  30581  omssubadd  30960  signsplypnf  31227  signsply0  31228  rpsqrtcn  31273  taupilem2  33764  taupi  33765  ptrecube  34035  heicant  34070  totbndbnd  34212  rpexpmord  38472  seff  39464  rpssxr  40616  ioorrnopnlem  41448  vonioolem1  41821  elbigolo1  43366  amgmwlem  43654  amgmlemALT  43655