Theorem rpre 10574

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 10569	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3388	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3338	. 2 |- RR+ C_ RR
4	3	sseli 3304	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1721   {crab 2670   class class class wbr 4172   RRcr 8945   0cc0 8946   < clt 9076   RR+crp 10568

This theorem is referenced by:  rpxr  10575  rpcn  10576  rpssre  10578  rpge0  10580  rprege0  10582  rprene0  10584  rpaddcl  10588  rpmulcl  10589  rpdivcl  10590  rpgecl  10593  xralrple  10747  xlemul1  10825  iccdil  10990  modcl  11208  mod0  11210  modge0  11212  modlt  11213  modabs  11229  modabs2  11230  modcyc  11231  moddi  11239  modsubdir  11240  modirr  11241  expnlbnd  11464  rennim  11999  cnpart  12000  sqrlem1  12003  sqrlem2  12004  sqrlem4  12006  sqrlem5  12007  sqrlem6  12008  sqrlem7  12009  resqrex  12011  rpsqrcl  12025  sqreulem  12118  eqsqr2d  12127  2clim  12321  reccn2  12345  cn1lem  12346  climsqz  12389  climsqz2  12390  rlimsqzlem  12397  climsup  12418  climcau  12419  caucvgrlem2  12423  iseralt  12433  cvgcmp  12550  cvgcmpce  12552  divrcnv  12587  efgt1  12672  ef01bndlem  12740  sinltx  12745  prmreclem6  13244  stdbdmet  18499  stdbdmopn  18501  met2ndci  18505  cfilucfilOLD  18552  cfilucfil  18553  ngptgp  18630  reperflem  18802  iccntr  18805  reconnlem2  18811  opnreen  18815  metdseq0  18837  xlebnum  18943  cphsqrcl3  19103  iscmet3lem3  19196  iscmet3lem1  19197  iscmet3lem2  19198  caubl  19213  lmcau  19218  bcthlem4  19233  minveclem3b  19282  minveclem3  19283  ivthlem2  19302  ivthlem3  19303  nulmbl2  19384  opnmbllem  19446  itg2const2  19586  itg2mulclem  19591  dveflem  19816  lhop  19853  dvcnvre  19856  aalioulem2  20203  aaliou  20208  aaliou3lem4  20216  ulmcaulem  20263  ulmcau  20264  ulmcn  20268  itgulm  20277  reeff1o  20316  pilem2  20321  logleb  20451  logcj  20454  argimgt0  20460  logdmnrp  20485  logcnlem3  20488  logcnlem4  20489  advlog  20498  efopnlem1  20500  cxple2  20541  cxplt2  20542  cxple3  20545  cxpcn3  20585  resqrcn  20586  asinneg  20679  atanbndlem  20718  cxplim  20763  cxp2limlem  20767  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  logdiflbnd  20786  harmoniclbnd  20800  harmonicbnd4  20802  chtrpcl  20911  ppiltx  20913  chtleppi  20947  logfacubnd  20958  logfaclbnd  20959  logfacbnd3  20960  logexprlim  20962  bposlem7  21027  bposlem8  21028  bposlem9  21029  chebbnd1  21119  chtppilim  21122  chto1ub  21123  chpo1ub  21127  vmadivsum  21129  rpvmasumlem  21134  dchrisumlem3  21138  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0  21167  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  mulog2sumlem2  21182  log2sumbnd  21191  selberglem2  21193  selberglem3  21194  selberg  21195  selberg2lem  21197  selberg2  21198  pntrf  21210  pntrmax  21211  pntrsumo1  21212  selbergr  21215  selbergs  21221  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntibndlem1  21236  pntlem3  21256  pntlemp  21257  pntleml  21258  pnt2  21260  padicabvcxp  21279  vacn  22143  nmcvcn  22144  smcnlem  22146  blocnilem  22258  chscllem2  23093  nmcexi  23482  nmcopexi  23483  nmcfnexi  23507  pnfinf  24206  sqsscirc1  24259  dya2icoseg2  24581  probfinmeasbOLD  24639  probfinmeasb  24640  subfacval3  24828  rprisefaccl  25291  mblfinlem  26143  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  areacirclem2  26181  areacirclem3  26182  areacirclem5  26185  areacirc  26187  opnrebl  26213  opnrebl2  26214  geomcau  26355  isbnd2  26382  ssbnd  26387  heiborlem7  26416  heiborlem8  26417  bfplem2  26422  rrncmslem  26431  rrnequiv  26434  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem5  26779  rpexpmord  26901  climinf  27599  stoweidlem7  27623

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-in 3287  df-ss 3294  df-rp 10569