Theorem rpre 9996

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 9990	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3325	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3272	. 2 |- RR+ C_ RR
4	3	sseli 3236	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2205   {crab 2526   class class class wbr 4111   RRcr 8128   0cc0 8129   < clt 8310   RR+crp 9989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-in 3219  df-ss 3226  df-rp 9990

This theorem is referenced by:  rpxr  9997  rpcn  9998  rpssre  10000  rpge0  10002  rprege0  10004  rpap0  10006  rprene0  10007  rpreap0  10008  rpaddcl  10013  rpmulcl  10014  rpdivcl  10015  rpgecl  10018  ledivge1le  10062  addlelt  10104  iccdil  10334  expnlbnd  11030  caucvgre  11670  rennim  11691  rpsqrtcl  11730  qdenre  11891  rpmaxcl  11912  rpmincl  11927  xrminrpcl  11963  2clim  11990  cn1lem  12003  climsqz  12024  climsqz2  12025  climcau  12036  efgt1  12387  ef01bndlem  12446  sinltxirr  12451  bdmet  15384  bdmopn  15386  dveflem  15608  reeff1o  15655  logleb  15757  logrpap0b  15758  cxple3  15803  rpcxpsqrt  15804  rpcxpsqrtth  15812  dceqnconst  16863  dcapnconst  16864