Theorem rpre 11238

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 11233	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3590	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3539	. 2 |- RR+ C_ RR
4	3	sseli 3505	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1767   {crab 2821   class class class wbr 4453   RRcr 9503   0cc0 9504   < clt 9640   RR+crp 11232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826  df-in 3488  df-ss 3495  df-rp 11233

This theorem is referenced by:  rpxr  11239  rpcn  11240  rpssre  11242  rpge0  11244  rprege0  11246  rprene0  11248  rpaddcl  11252  rpmulcl  11253  rpdivcl  11254  rpgecl  11257  xralrple  11416  xlemul1  11494  iccdil  11670  ltdifltdiv  11946  modcl  11980  mod0  11983  modge0  11985  modlt  11986  modid0  12001  modabs  12009  modabs2  12010  modcyc  12011  modltm1p1mod  12019  2txmodxeq0  12027  2submod  12028  moddi  12034  modsubdir  12035  modeqmodmin  12036  modirr  12037  expnlbnd  12276  rennim  13052  cnpart  13053  sqrlem1  13056  sqrlem2  13057  sqrlem4  13059  sqrlem5  13060  sqrlem6  13061  sqrlem7  13062  resqrex  13064  rpsqrtcl  13078  sqreulem  13172  eqsqrt2d  13181  2clim  13375  reccn2  13399  cn1lem  13400  climsqz  13443  climsqz2  13444  rlimsqzlem  13451  climsup  13472  climcau  13473  caucvgrlem2  13477  iseralt  13487  cvgcmp  13610  cvgcmpce  13612  divrcnv  13644  efgt1  13729  ef01bndlem  13797  sinltx  13802  stdbdmet  20887  stdbdmopn  20889  met2ndci  20893  cfilucfilOLD  20940  cfilucfil  20941  ngptgp  21018  reperflem  21191  iccntr  21194  reconnlem2  21200  opnreen  21204  metdseq0  21226  xlebnum  21333  cphsqrtcl3  21502  iscmet3lem3  21597  iscmet3lem1  21598  iscmet3lem2  21599  caubl  21614  lmcau  21619  bcthlem4  21634  minveclem3b  21711  minveclem3  21712  ivthlem2  21732  ivthlem3  21733  nulmbl2  21815  opnmbllem  21878  itg2const2  22016  itg2mulclem  22021  dveflem  22248  lhop  22285  dvcnvre  22288  aalioulem2  22596  aaliou  22601  aaliou3lem4  22609  ulmcaulem  22656  ulmcau  22657  ulmcn  22661  itgulm  22670  reeff1o  22709  pilem2  22714  logleb  22854  logcj  22857  argimgt0  22863  logdmnrp  22888  logcnlem3  22891  logcnlem4  22892  advlog  22901  efopnlem1  22903  cxple2  22944  cxplt2  22945  cxple3  22948  cxpcn3  22988  resqrtcn  22989  asinneg  23083  atanbndlem  23122  cxplim  23167  cxp2limlem  23171  cxp2lim  23172  cxploglim  23173  cxploglim2  23174  logdiflbnd  23190  harmoniclbnd  23204  harmonicbnd4  23206  chtrpcl  23315  ppiltx  23317  chtleppi  23351  logfacubnd  23362  logfaclbnd  23363  logfacbnd3  23364  logexprlim  23366  bposlem7  23431  bposlem8  23432  bposlem9  23433  chebbnd1  23523  chtppilim  23526  chto1ub  23527  chpo1ub  23531  vmadivsum  23533  rpvmasumlem  23538  dchrisumlem3  23542  dchrvmasumlem2  23549  dchrvmasumiflem1  23552  dchrisum0  23571  mudivsum  23581  mulogsumlem  23582  mulogsum  23583  mulog2sumlem2  23586  log2sumbnd  23595  selberglem2  23597  selberglem3  23598  selberg  23599  selberg2lem  23601  selberg2  23602  pntrf  23614  pntrmax  23615  pntrsumo1  23616  selbergr  23619  selbergs  23625  pntrlog2bndlem4  23631  pntrlog2bndlem5  23632  pntibndlem1  23640  pntlem3  23660  pntlemp  23661  pntleml  23662  pnt2  23664  padicabvcxp  23683  vacn  25427  nmcvcn  25428  smcnlem  25430  blocnilem  25542  chscllem2  26379  nmcexi  26768  nmcopexi  26769  nmcfnexi  26793  pnfinf  27551  sqsscirc1  27715  dya2icoseg2  28074  probfinmeasbOLD  28192  probfinmeasb  28193  subfacval3  28458  rprisefaccl  29072  opnmbllem0  29977  itg2addnclem  29993  itg2addnclem2  29994  itg2addnclem3  29995  itg2addnc  29996  itg2gt0cn  29997  ftc1anclem5  30021  ftc1anclem7  30023  ftc1anc  30025  areacirclem1  30034  areacirclem4  30037  areacirc  30039  opnrebl  30065  opnrebl2  30066  geomcau  30179  isbnd2  30206  ssbnd  30211  heiborlem7  30240  heiborlem8  30241  bfplem2  30246  rrncmslem  30255  rrnequiv  30258  irrapxlem1  30686  irrapxlem2  30687  irrapxlem3  30688  irrapxlem5  30690  rpexpmord  30812  neglt  31367  2timesgt  31375  climinf  31471  mullimc  31481  mullimcf  31488  limcrecl  31494  limcleqr  31509  addlimc  31513  0ellimcdiv  31514  limclner  31516  ioodvbdlimc1lem1  31584  ioodvbdlimc1lem2  31585  ioodvbdlimc2lem  31587  stoweidlem7  31630  fourierdlem45  31775  fourierdlem73  31803  fourierdlem87  31817  fourierdlem103  31833  fourierdlem104  31834  taupilem1  37168