Theorem rpre 7236

Description: A positive real is a real.

Assertion

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

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		df-rp 7232	. . 3 |- RR+ = {x e. RR | 0 < x}
2		ssrab2 2692	. . 3 |- {x e. RR | 0 < x} C_ RR
3	1, 2	eqsstri 2647	. 2 |- RR+ C_ RR
4	3	sseli 2617	1 |- (A e. RR+ -> A e. RR)

Syntax hints:   -> wi 3   e. wcel 1300  {crab 2108   class class class wbr 3338  RRcr 6385  0cc0 6386  RR+crp 6453   < clt 6653

This theorem is referenced by:  rpcn 7237  rpssre 7239  rpge0 7241  rpregt0 7242  rprene0 7244  rpaddcl 7247  rpmulcl 7248  rpdivcl 7249  modcl 7502  modge0 7503  modlt 7504  modmulnn 7510  modabs 7514  modabs2 7515  modcyc 7516  moddi 7520  modsubdir 7521  modirr 7522  expnlbnd 7902  expnlbnd2 7903  rpsqrcl 7965  abscncflem 8536  ivthlem6 8548  ivthlem7 8549  minveclem24 9913  minveclem25 9914  minveclem26 9915  minveclem27 9916  minveclem28 9917  pire 10026  subtopmet 10256  cbci 14852  mslb1 15007  2wsms 15008  iintlem1 15010  iint 15012  mod0 15800  fsumltisumii 15822  blssp 15844  geomcau 15849  iccdil 15861  totbndbnd 15944  heiborlem16 15970  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem36 15990  bfplem6 16003  bfplem7 16004  bfplem8 16005  bfplem9 16006  bfplem11 16008  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112  df-in 2603  df-ss 2605  df-rp 7232

Copyright terms: Public domain