Theorem rpret 6285

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 6282	. . 3 |- RR+ = {x e. RR | 0 < x}
2		ssrab2 2134	. . 3 |- {x e. RR | 0 < x} (_ RR
3	1, 2	eqsstr 2094	. 2 |- RR+ (_ RR
4	3	sseli 2068	1 |- (A e. RR+ -> A e. RR)

Syntax hints:   -> wi 3   e. wcel 960  {crab 1651   class class class wbr 2624  RRcr 5245  0cc0 5246  RR+crp 5312   < clt 5498

This theorem is referenced by:  rpssre 6286  rpge0t 6288  rpne0t 6289  rpaddclt 6291  rpmulclt 6292  rpdivclt 6293  expnlbndt 6656  rpsqrclt 6716  abscncflem 7274  ivthlem6 7286  ivthlem7 7287  minveclem24 8564  minveclem25 8565  minveclem26 8566  minveclem27 8567  minveclem28 8568  pire 8672  reeflogt 8756  relogeftb 8760  mslb1 10600  2wsms 10601  iintlem1 10603  iint 10605

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-rab 1655  df-in 2054  df-ss 2056  df-rp 6282

Copyright terms: Public domain