Theorem rpre 11336

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 11331	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3525	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3473	. 2 |- RR+ C_ RR
4	3	sseli 3439	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1897   {crab 2752   class class class wbr 4415   RRcr 9563   0cc0 9564   < clt 9700   RR+crp 11330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-in 3422  df-ss 3429  df-rp 11331

This theorem is referenced by:  rpxr  11337  rpcn  11338  rpssre  11340  rpge0  11342  rprege0  11344  rprene0  11346  rpaddcl  11351  rpmulcl  11352  rpdivcl  11353  rpgecl  11356  xralrple  11526  xlemul1  11604  infmrp1  11662  iccdil  11798  ltdifltdiv  12097  modcl  12131  mod0  12134  mulmod0  12135  modge0  12137  modlt  12138  modid0  12153  modabs  12161  modabs2  12162  modcyc  12163  modltm1p1mod  12173  2txmodxeq0  12181  2submod  12182  moddi  12188  modsubdir  12189  modeqmodmin  12190  modirr  12191  expnlbnd  12433  rennim  13350  cnpart  13351  sqrlem1  13354  sqrlem2  13355  sqrlem4  13357  sqrlem5  13358  sqrlem6  13359  sqrlem7  13360  resqrex  13362  rpsqrtcl  13376  sqreulem  13470  eqsqrt2d  13479  2clim  13684  reccn2  13708  cn1lem  13709  climsqz  13752  climsqz2  13753  rlimsqzlem  13760  climsup  13781  climcau  13782  caucvgrlem2  13788  iseralt  13799  cvgcmp  13924  cvgcmpce  13926  divrcnv  13958  rprisefaccl  14124  efgt1  14218  ef01bndlem  14286  sinltx  14291  stdbdmet  21579  stdbdmopn  21581  met2ndci  21585  cfilucfil  21622  ngptgp  21692  reperflem  21884  iccntr  21887  reconnlem2  21893  opnreen  21897  metdseq0  21919  metdseq0OLD  21934  xlebnum  22044  cphsqrtcl3  22213  iscmet3lem3  22308  iscmet3lem1  22309  iscmet3lem2  22310  caubl  22325  lmcau  22330  bcthlem4  22343  minveclem3b  22418  minveclem3  22419  minveclem3bOLD  22430  minveclem3OLD  22431  ivthlem2  22451  ivthlem3  22452  nulmbl2  22538  opnmbllem  22607  itg2const2  22747  itg2mulclem  22752  dveflem  22979  lhop  23016  dvcnvre  23019  aalioulem2  23337  aaliou  23342  aaliou3lem4  23350  ulmcaulem  23397  ulmcau  23398  ulmcn  23402  itgulm  23411  reeff1o  23450  pilem2  23455  pilem2OLD  23456  logleb  23600  logcj  23603  argimgt0  23609  logdmnrp  23634  logcnlem3  23637  logcnlem4  23638  advlog  23647  efopnlem1  23649  cxple2  23690  cxplt2  23691  cxple3  23694  cxpcn3  23736  resqrtcn  23737  relogbf  23776  asinneg  23860  atanbndlem  23899  cxplim  23945  cxp2limlem  23949  cxp2lim  23950  cxploglim  23951  cxploglim2  23952  logdiflbnd  23968  harmoniclbnd  23982  harmonicbnd4  23984  chtrpcl  24150  ppiltx  24152  chtleppi  24186  logfacubnd  24197  logfaclbnd  24198  logfacbnd3  24199  logexprlim  24201  bposlem7  24266  bposlem8  24267  bposlem9  24268  chebbnd1  24358  chtppilim  24361  chto1ub  24362  chpo1ub  24366  vmadivsum  24368  rpvmasumlem  24373  dchrisumlem3  24377  dchrvmasumlem2  24384  dchrvmasumiflem1  24387  dchrisum0  24406  mudivsum  24416  mulogsumlem  24417  mulogsum  24418  mulog2sumlem2  24421  log2sumbnd  24430  selberglem2  24432  selberglem3  24433  selberg  24434  selberg2lem  24436  selberg2  24437  pntrf  24449  pntrmax  24450  pntrsumo1  24451  selbergr  24454  selbergs  24460  pntrlog2bndlem4  24466  pntrlog2bndlem5  24467  pntibndlem1  24475  pntlem3  24495  pntlemp  24496  pntleml  24497  pnt2  24499  padicabvcxp  24518  vacn  26378  nmcvcn  26379  smcnlem  26381  blocnilem  26493  chscllem2  27339  nmcexi  27727  nmcopexi  27728  nmcfnexi  27752  pnfinf  28548  sqsscirc1  28762  dya2icoseg2  29148  probfinmeasbOLD  29309  probfinmeasb  29310  subfacval3  29960  opnrebl  31024  opnrebl2  31025  taupilem1  31766  opnmbllem0  32020  itg2addnclem  32037  itg2addnclem2  32038  itg2addnclem3  32039  itg2addnc  32040  itg2gt0cn  32041  ftc1anclem5  32065  ftc1anclem7  32067  ftc1anc  32069  areacirclem1  32076  areacirclem4  32079  areacirc  32081  geomcau  32132  isbnd2  32159  ssbnd  32164  heiborlem7  32193  heiborlem8  32194  bfplem2  32199  rrncmslem  32208  rrnequiv  32211  irrapxlem1  35710  irrapxlem2  35711  irrapxlem3  35712  irrapxlem5  35714  rpexpmord  35840  neglt  37531  2timesgt  37538  supxrge  37598  suplesup  37599  xrlexaddrp  37612  xralrple2  37614  climinf  37721  climinfOLD  37722  mullimc  37733  mullimcf  37740  limcrecl  37746  limcleqr  37762  addlimc  37766  0ellimcdiv  37767  limclner  37769  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem1OLD  37842  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  stoweidlem7  37904  fourierdlem73  38080  fourierdlem87  38094  fourierdlem103  38110  fourierdlem104  38111  sge0iunmptlemre  38294  fldivexpfllog2  40648  blenre  40657