Theorem rpre 9956

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 9950	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3313	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3260	. 2 |- RR+ C_ RR
4	3	sseli 3224	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2202   {crab 2515   class class class wbr 4093   RRcr 8091   0cc0 8092   < clt 8273   RR+crp 9949

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-in 3207  df-ss 3214  df-rp 9950

This theorem is referenced by:  rpxr  9957  rpcn  9958  rpssre  9960  rpge0  9962  rprege0  9964  rpap0  9966  rprene0  9967  rpreap0  9968  rpaddcl  9973  rpmulcl  9974  rpdivcl  9975  rpgecl  9978  ledivge1le  10022  addlelt  10064  iccdil  10294  expnlbnd  10989  caucvgre  11621  rennim  11642  rpsqrtcl  11681  qdenre  11842  rpmaxcl  11863  rpmincl  11878  xrminrpcl  11914  2clim  11941  cn1lem  11954  climsqz  11975  climsqz2  11976  climcau  11987  efgt1  12338  ef01bndlem  12397  sinltxirr  12402  bdmet  15313  bdmopn  15315  dveflem  15537  reeff1o  15584  logleb  15686  logrpap0b  15687  cxple3  15732  rpcxpsqrt  15733  rpcxpsqrtth  15741  dceqnconst  16793  dcapnconst  16794