Theorem rpret 6284

Description: A positive real is a real.

Assertion

Ref	Expression
rpret	|- (A e. RR+ -> A e. RR)

Proof of Theorem rpret

Step	Hyp	Ref	Expression
1		df-rp 6281	. . 3 |- RR+ = {x e. RR | 0 < x}
2		ssrab2 2131	. . 3 |- {x e. RR | 0 < x} (_ RR
3	1, 2	eqsstr 2091	. 2 |- RR+ (_ RR
4	3	sseli 2065	1 |- (A e. RR+ -> A e. RR)

Syntax hints:   -> wi 3   e. wcel 958  {crab 1648   class class class wbr 2619  RRcr 5233  0cc0 5234  RR+crp 5300   < clt 5486

This theorem is referenced by:  rpssre 6285  rpge0t 6287  rpne0t 6288  rpaddclt 6290  rpmulclt 6291  rpdivclt 6292  expnlbndt 6655  rpsqrclt 6715  abscncflem 7274  ivthlem6 7286  ivthlem7 7287  minveclem24 8568  minveclem25 8569  minveclem26 8570  minveclem27 8571  minveclem28 8572  pire 8677  reeflogt 8761  relogeftb 8765  mslb1 10629  2wsms 10630  iintlem1 10632  iint 10634

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rab 1652  df-in 2051  df-ss 2053  df-rp 6281

Copyright terms: Public domain