Theorem rpre 9690

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 9684	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3255	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3202	. 2 |- RR+ C_ RR
4	3	sseli 3166	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2160   {crab 2472   class class class wbr 4018   RRcr 7840   0cc0 7841   < clt 8022   RR+crp 9683

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rab 2477  df-in 3150  df-ss 3157  df-rp 9684

This theorem is referenced by:  rpxr  9691  rpcn  9692  rpssre  9694  rpge0  9696  rprege0  9698  rpap0  9700  rprene0  9701  rpreap0  9702  rpaddcl  9707  rpmulcl  9708  rpdivcl  9709  rpgecl  9712  ledivge1le  9756  addlelt  9798  iccdil  10028  expnlbnd  10676  caucvgre  11022  rennim  11043  rpsqrtcl  11082  qdenre  11243  rpmaxcl  11264  rpmincl  11278  xrminrpcl  11314  2clim  11341  cn1lem  11354  climsqz  11375  climsqz2  11376  climcau  11387  efgt1  11737  ef01bndlem  11796  bdmet  14459  bdmopn  14461  dveflem  14644  reeff1o  14651  logleb  14753  logrpap0b  14754  cxple3  14798  rpcxpsqrt  14799  rpcxpsqrtth  14807  dceqnconst  15267  dcapnconst  15268