Theorem rpre 10984

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 10979	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3425	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3374	. 2 |- RR+ C_ RR
4	3	sseli 3340	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1755   {crab 2709   class class class wbr 4280   RRcr 9268   0cc0 9269   < clt 9405   RR+crp 10978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-in 3323  df-ss 3330  df-rp 10979

This theorem is referenced by:  rpxr  10985  rpcn  10986  rpssre  10988  rpge0  10990  rprege0  10992  rprene0  10994  rpaddcl  10998  rpmulcl  10999  rpdivcl  11000  rpgecl  11003  xralrple  11162  xlemul1  11240  iccdil  11409  ltdifltdiv  11661  modcl  11695  mod0  11698  modge0  11700  modlt  11701  modid0  11716  modabs  11724  modabs2  11725  modcyc  11726  modltm1p1mod  11734  2txmodxeq0  11742  2submod  11743  moddi  11749  modsubdir  11750  modeqmodmin  11751  modirr  11752  expnlbnd  11977  rennim  12711  cnpart  12712  sqrlem1  12715  sqrlem2  12716  sqrlem4  12718  sqrlem5  12719  sqrlem6  12720  sqrlem7  12721  resqrex  12723  rpsqrcl  12737  sqreulem  12830  eqsqr2d  12839  2clim  13033  reccn2  13057  cn1lem  13058  climsqz  13101  climsqz2  13102  rlimsqzlem  13109  climsup  13130  climcau  13131  caucvgrlem2  13135  iseralt  13145  cvgcmp  13261  cvgcmpce  13263  divrcnv  13297  efgt1  13382  ef01bndlem  13450  sinltx  13455  stdbdmet  19932  stdbdmopn  19934  met2ndci  19938  cfilucfilOLD  19985  cfilucfil  19986  ngptgp  20063  reperflem  20236  iccntr  20239  reconnlem2  20245  opnreen  20249  metdseq0  20271  xlebnum  20378  cphsqrcl3  20547  iscmet3lem3  20642  iscmet3lem1  20643  iscmet3lem2  20644  caubl  20659  lmcau  20664  bcthlem4  20679  minveclem3b  20756  minveclem3  20757  ivthlem2  20777  ivthlem3  20778  nulmbl2  20859  opnmbllem  20922  itg2const2  21060  itg2mulclem  21065  dveflem  21292  lhop  21329  dvcnvre  21332  aalioulem2  21683  aaliou  21688  aaliou3lem4  21696  ulmcaulem  21743  ulmcau  21744  ulmcn  21748  itgulm  21757  reeff1o  21796  pilem2  21801  logleb  21936  logcj  21939  argimgt0  21945  logdmnrp  21970  logcnlem3  21973  logcnlem4  21974  advlog  21983  efopnlem1  21985  cxple2  22026  cxplt2  22027  cxple3  22030  cxpcn3  22070  resqrcn  22071  asinneg  22165  atanbndlem  22204  cxplim  22249  cxp2limlem  22253  cxp2lim  22254  cxploglim  22255  cxploglim2  22256  logdiflbnd  22272  harmoniclbnd  22286  harmonicbnd4  22288  chtrpcl  22397  ppiltx  22399  chtleppi  22433  logfacubnd  22444  logfaclbnd  22445  logfacbnd3  22446  logexprlim  22448  bposlem7  22513  bposlem8  22514  bposlem9  22515  chebbnd1  22605  chtppilim  22608  chto1ub  22609  chpo1ub  22613  vmadivsum  22615  rpvmasumlem  22620  dchrisumlem3  22624  dchrvmasumlem2  22631  dchrvmasumiflem1  22634  dchrisum0  22653  mudivsum  22663  mulogsumlem  22664  mulogsum  22665  mulog2sumlem2  22668  log2sumbnd  22677  selberglem2  22679  selberglem3  22680  selberg  22681  selberg2lem  22683  selberg2  22684  pntrf  22696  pntrmax  22697  pntrsumo1  22698  selbergr  22701  selbergs  22707  pntrlog2bndlem4  22713  pntrlog2bndlem5  22714  pntibndlem1  22722  pntlem3  22742  pntlemp  22743  pntleml  22744  pnt2  22746  padicabvcxp  22765  vacn  23911  nmcvcn  23912  smcnlem  23914  blocnilem  24026  chscllem2  24863  nmcexi  25252  nmcopexi  25253  nmcfnexi  25277  pnfinf  26023  sqsscirc1  26191  dya2icoseg2  26546  probfinmeasbOLD  26658  probfinmeasb  26659  subfacval3  26924  rprisefaccl  27372  opnmbllem0  28268  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2addnc  28287  itg2gt0cn  28288  ftc1anclem5  28312  ftc1anclem7  28314  ftc1anc  28316  areacirclem1  28325  areacirclem4  28328  areacirc  28330  opnrebl  28356  opnrebl2  28357  geomcau  28496  isbnd2  28523  ssbnd  28528  heiborlem7  28557  heiborlem8  28558  bfplem2  28563  rrncmslem  28572  rrnequiv  28575  irrapxlem1  29005  irrapxlem2  29006  irrapxlem3  29007  irrapxlem5  29009  rpexpmord  29131  climinf  29622  stoweidlem7  29645  taupilem1  35185