Theorem rpre 11251

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 11246	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3581	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3529	. 2 |- RR+ C_ RR
4	3	sseli 3495	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1819   {crab 2811   class class class wbr 4456   RRcr 9508   0cc0 9509   < clt 9645   RR+crp 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-in 3478  df-ss 3485  df-rp 11246

This theorem is referenced by:  rpxr  11252  rpcn  11253  rpssre  11255  rpge0  11257  rprege0  11259  rprene0  11261  rpaddcl  11265  rpmulcl  11266  rpdivcl  11267  rpgecl  11270  xralrple  11429  xlemul1  11507  iccdil  11683  ltdifltdiv  11968  modcl  12002  mod0  12005  modge0  12007  modlt  12008  modid0  12023  modabs  12031  modabs2  12032  modcyc  12033  modltm1p1mod  12041  2txmodxeq0  12049  2submod  12050  moddi  12056  modsubdir  12057  modeqmodmin  12058  modirr  12059  expnlbnd  12298  rennim  13083  cnpart  13084  sqrlem1  13087  sqrlem2  13088  sqrlem4  13090  sqrlem5  13091  sqrlem6  13092  sqrlem7  13093  resqrex  13095  rpsqrtcl  13109  sqreulem  13203  eqsqrt2d  13212  2clim  13406  reccn2  13430  cn1lem  13431  climsqz  13474  climsqz2  13475  rlimsqzlem  13482  climsup  13503  climcau  13504  caucvgrlem2  13508  iseralt  13518  cvgcmp  13641  cvgcmpce  13643  divrcnv  13675  efgt1  13862  ef01bndlem  13930  sinltx  13935  stdbdmet  21144  stdbdmopn  21146  met2ndci  21150  cfilucfilOLD  21197  cfilucfil  21198  ngptgp  21275  reperflem  21448  iccntr  21451  reconnlem2  21457  opnreen  21461  metdseq0  21483  xlebnum  21590  cphsqrtcl3  21759  iscmet3lem3  21854  iscmet3lem1  21855  iscmet3lem2  21856  caubl  21871  lmcau  21876  bcthlem4  21891  minveclem3b  21968  minveclem3  21969  ivthlem2  21989  ivthlem3  21990  nulmbl2  22072  opnmbllem  22135  itg2const2  22273  itg2mulclem  22278  dveflem  22505  lhop  22542  dvcnvre  22545  aalioulem2  22854  aaliou  22859  aaliou3lem4  22867  ulmcaulem  22914  ulmcau  22915  ulmcn  22919  itgulm  22928  reeff1o  22967  pilem2  22972  logleb  23113  logcj  23116  argimgt0  23122  logdmnrp  23147  logcnlem3  23150  logcnlem4  23151  advlog  23160  efopnlem1  23162  cxple2  23203  cxplt2  23204  cxple3  23207  cxpcn3  23247  resqrtcn  23248  asinneg  23342  atanbndlem  23381  cxplim  23426  cxp2limlem  23430  cxp2lim  23431  cxploglim  23432  cxploglim2  23433  logdiflbnd  23449  harmoniclbnd  23463  harmonicbnd4  23465  chtrpcl  23574  ppiltx  23576  chtleppi  23610  logfacubnd  23621  logfaclbnd  23622  logfacbnd3  23623  logexprlim  23625  bposlem7  23690  bposlem8  23691  bposlem9  23692  chebbnd1  23782  chtppilim  23785  chto1ub  23786  chpo1ub  23790  vmadivsum  23792  rpvmasumlem  23797  dchrisumlem3  23801  dchrvmasumlem2  23808  dchrvmasumiflem1  23811  dchrisum0  23830  mudivsum  23840  mulogsumlem  23841  mulogsum  23842  mulog2sumlem2  23845  log2sumbnd  23854  selberglem2  23856  selberglem3  23857  selberg  23858  selberg2lem  23860  selberg2  23861  pntrf  23873  pntrmax  23874  pntrsumo1  23875  selbergr  23878  selbergs  23884  pntrlog2bndlem4  23890  pntrlog2bndlem5  23891  pntibndlem1  23899  pntlem3  23919  pntlemp  23920  pntleml  23921  pnt2  23923  padicabvcxp  23942  vacn  25730  nmcvcn  25731  smcnlem  25733  blocnilem  25845  chscllem2  26682  nmcexi  27071  nmcopexi  27072  nmcfnexi  27096  pnfinf  27879  sqsscirc1  28043  dya2icoseg2  28410  probfinmeasbOLD  28542  probfinmeasb  28543  subfacval3  28808  rprisefaccl  29320  opnmbllem0  30212  itg2addnclem  30228  itg2addnclem2  30229  itg2addnclem3  30230  itg2addnc  30231  itg2gt0cn  30232  ftc1anclem5  30256  ftc1anclem7  30258  ftc1anc  30260  areacirclem1  30269  areacirclem4  30272  areacirc  30274  opnrebl  30300  opnrebl2  30301  geomcau  30414  isbnd2  30441  ssbnd  30446  heiborlem7  30475  heiborlem8  30476  bfplem2  30481  rrncmslem  30490  rrnequiv  30493  irrapxlem1  30920  irrapxlem2  30921  irrapxlem3  30922  irrapxlem5  30924  rpexpmord  31046  neglt  31628  2timesgt  31636  climinf  31773  mullimc  31783  mullimcf  31790  limcrecl  31796  limcleqr  31811  addlimc  31815  0ellimcdiv  31816  limclner  31818  ioodvbdlimc1lem1  31889  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  stoweidlem7  31950  fourierdlem73  32123  fourierdlem87  32137  fourierdlem103  32153  fourierdlem104  32154  taupilem1  37797