Theorem rpre 9239

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 9234	. . 3 |- RR+ = { x e. RR | 0 < x }
2		ssrab2 3121	. . 3 |- { x e. RR | 0 < x } C_ RR
3	1, 2	eqsstri 3071	. 2 |- RR+ C_ RR
4	3	sseli 3035	1 |- ( A e. RR+ -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1445   {crab 2374   class class class wbr 3867   RRcr 7446   0cc0 7447   < clt 7619   RR+crp 9233

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rab 2379  df-in 3019  df-ss 3026  df-rp 9234

This theorem is referenced by:  rpxr  9240  rpcn  9241  rpssre  9243  rpge0  9245  rprege0  9247  rpap0  9249  rprene0  9250  rpreap0  9251  rpaddcl  9256  rpmulcl  9257  rpdivcl  9258  rpgecl  9261  ledivge1le  9302  addlelt  9338  iccdil  9564  expnlbnd  10193  caucvgre  10529  rennim  10550  rpsqrtcl  10589  qdenre  10750  rpmincl  10784  xrminrpcl  10817  2clim  10844  cn1lem  10857  climsqz  10878  climsqz2  10879  climcau  10890  efgt1  11136  ef01bndlem  11196  bdmet  12288  bdmopn  12290