Theorem rpre 10996

Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.)

Assertion

Ref	Expression
rpre	|- ( A e. RR+ -> A e. RR )

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		df-rp 10991	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3436	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3385	. 2 |- RR+ C_ RR
4	3	sseli 3351	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1756   {crab 2718   class class class wbr 4291   RRcr 9280   0cc0 9281   < clt 9417   RR+crp 10990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2723  df-in 3334  df-ss 3341  df-rp 10991

This theorem is referenced by:  rpxr  10997  rpcn  10998  rpssre  11000  rpge0  11002  rprege0  11004  rprene0  11006  rpaddcl  11010  rpmulcl  11011  rpdivcl  11012  rpgecl  11015  xralrple  11174  xlemul1  11252  iccdil  11422  ltdifltdiv  11677  modcl  11711  mod0  11714  modge0  11716  modlt  11717  modid0  11732  modabs  11740  modabs2  11741  modcyc  11742  modltm1p1mod  11750  2txmodxeq0  11758  2submod  11759  moddi  11765  modsubdir  11766  modeqmodmin  11767  modirr  11768  expnlbnd  11993  rennim  12727  cnpart  12728  sqrlem1  12731  sqrlem2  12732  sqrlem4  12734  sqrlem5  12735  sqrlem6  12736  sqrlem7  12737  resqrex  12739  rpsqrcl  12753  sqreulem  12846  eqsqr2d  12855  2clim  13049  reccn2  13073  cn1lem  13074  climsqz  13117  climsqz2  13118  rlimsqzlem  13125  climsup  13146  climcau  13147  caucvgrlem2  13151  iseralt  13161  cvgcmp  13278  cvgcmpce  13280  divrcnv  13314  efgt1  13399  ef01bndlem  13467  sinltx  13472  stdbdmet  20090  stdbdmopn  20092  met2ndci  20096  cfilucfilOLD  20143  cfilucfil  20144  ngptgp  20221  reperflem  20394  iccntr  20397  reconnlem2  20403  opnreen  20407  metdseq0  20429  xlebnum  20536  cphsqrcl3  20705  iscmet3lem3  20800  iscmet3lem1  20801  iscmet3lem2  20802  caubl  20817  lmcau  20822  bcthlem4  20837  minveclem3b  20914  minveclem3  20915  ivthlem2  20935  ivthlem3  20936  nulmbl2  21017  opnmbllem  21080  itg2const2  21218  itg2mulclem  21223  dveflem  21450  lhop  21487  dvcnvre  21490  aalioulem2  21798  aaliou  21803  aaliou3lem4  21811  ulmcaulem  21858  ulmcau  21859  ulmcn  21863  itgulm  21872  reeff1o  21911  pilem2  21916  logleb  22051  logcj  22054  argimgt0  22060  logdmnrp  22085  logcnlem3  22088  logcnlem4  22089  advlog  22098  efopnlem1  22100  cxple2  22141  cxplt2  22142  cxple3  22145  cxpcn3  22185  resqrcn  22186  asinneg  22280  atanbndlem  22319  cxplim  22364  cxp2limlem  22368  cxp2lim  22369  cxploglim  22370  cxploglim2  22371  logdiflbnd  22387  harmoniclbnd  22401  harmonicbnd4  22403  chtrpcl  22512  ppiltx  22514  chtleppi  22548  logfacubnd  22559  logfaclbnd  22560  logfacbnd3  22561  logexprlim  22563  bposlem7  22628  bposlem8  22629  bposlem9  22630  chebbnd1  22720  chtppilim  22723  chto1ub  22724  chpo1ub  22728  vmadivsum  22730  rpvmasumlem  22735  dchrisumlem3  22739  dchrvmasumlem2  22746  dchrvmasumiflem1  22749  dchrisum0  22768  mudivsum  22778  mulogsumlem  22779  mulogsum  22780  mulog2sumlem2  22783  log2sumbnd  22792  selberglem2  22794  selberglem3  22795  selberg  22796  selberg2lem  22798  selberg2  22799  pntrf  22811  pntrmax  22812  pntrsumo1  22813  selbergr  22816  selbergs  22822  pntrlog2bndlem4  22828  pntrlog2bndlem5  22829  pntibndlem1  22837  pntlem3  22857  pntlemp  22858  pntleml  22859  pnt2  22861  padicabvcxp  22880  vacn  24088  nmcvcn  24089  smcnlem  24091  blocnilem  24203  chscllem2  25040  nmcexi  25429  nmcopexi  25430  nmcfnexi  25454  pnfinf  26199  sqsscirc1  26337  dya2icoseg2  26692  probfinmeasbOLD  26810  probfinmeasb  26811  subfacval3  27076  rprisefaccl  27525  opnmbllem0  28425  itg2addnclem  28441  itg2addnclem2  28442  itg2addnclem3  28443  itg2addnc  28444  itg2gt0cn  28445  ftc1anclem5  28469  ftc1anclem7  28471  ftc1anc  28473  areacirclem1  28482  areacirclem4  28485  areacirc  28487  opnrebl  28513  opnrebl2  28514  geomcau  28653  isbnd2  28680  ssbnd  28685  heiborlem7  28714  heiborlem8  28715  bfplem2  28720  rrncmslem  28729  rrnequiv  28732  irrapxlem1  29161  irrapxlem2  29162  irrapxlem3  29163  irrapxlem5  29165  rpexpmord  29287  climinf  29777  stoweidlem7  29800  taupilem1  35613