Theorem rpre 9817

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 9811	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3286	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3233	. 2 |- RR+ C_ RR
4	3	sseli 3197	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2178   {crab 2490   class class class wbr 4059   RRcr 7959   0cc0 7960   < clt 8142   RR+crp 9810

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rab 2495  df-in 3180  df-ss 3187  df-rp 9811

This theorem is referenced by:  rpxr  9818  rpcn  9819  rpssre  9821  rpge0  9823  rprege0  9825  rpap0  9827  rprene0  9828  rpreap0  9829  rpaddcl  9834  rpmulcl  9835  rpdivcl  9836  rpgecl  9839  ledivge1le  9883  addlelt  9925  iccdil  10155  expnlbnd  10846  caucvgre  11407  rennim  11428  rpsqrtcl  11467  qdenre  11628  rpmaxcl  11649  rpmincl  11664  xrminrpcl  11700  2clim  11727  cn1lem  11740  climsqz  11761  climsqz2  11762  climcau  11773  efgt1  12123  ef01bndlem  12182  sinltxirr  12187  bdmet  15089  bdmopn  15091  dveflem  15313  reeff1o  15360  logleb  15462  logrpap0b  15463  cxple3  15508  rpcxpsqrt  15509  rpcxpsqrtth  15517  dceqnconst  16201  dcapnconst  16202