Theorem rpre 9477

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 9471	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3187	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3134	. 2 |- RR+ C_ RR
4	3	sseli 3098	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1481   {crab 2421   class class class wbr 3937   RRcr 7643   0cc0 7644   < clt 7824   RR+crp 9470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rab 2426  df-in 3082  df-ss 3089  df-rp 9471

This theorem is referenced by:  rpxr  9478  rpcn  9479  rpssre  9481  rpge0  9483  rprege0  9485  rpap0  9487  rprene0  9488  rpreap0  9489  rpaddcl  9494  rpmulcl  9495  rpdivcl  9496  rpgecl  9499  ledivge1le  9543  addlelt  9585  iccdil  9811  expnlbnd  10447  caucvgre  10785  rennim  10806  rpsqrtcl  10845  qdenre  11006  rpmaxcl  11027  rpmincl  11041  xrminrpcl  11075  2clim  11102  cn1lem  11115  climsqz  11136  climsqz2  11137  climcau  11148  efgt1  11440  ef01bndlem  11499  bdmet  12710  bdmopn  12712  dveflem  12895  reeff1o  12902  logleb  13004  logrpap0b  13005  cxple3  13049  rpcxpsqrt  13050  rpcxpsqrtth  13058  dceqnconst  13423