Theorem elrp 6107

Description: Membership in the set of positive reals.

Assertion

Ref	Expression
elrp	|- (A e. RR+ <-> (A e. RR /\ 0 < A))

Proof of Theorem elrp

Step	Hyp	Ref	Expression
1		breq2 2678	. 2 |- (x = A -> (0 < x <-> 0 < A))
2		df-rp 6106	. 2 |- RR+ = {x e. RR | 0 < x}
3	1, 2	elrab2 1954	1 |- (A e. RR+ <-> (A e. RR /\ 0 < A))

Syntax hints:   <-> wb 153   /\ wa 230   e. wcel 999   class class class wbr 2674  RRcr 5298  0cc0 5299  RR+crp 5365   < clt 5551

This theorem is referenced by:  elrpii 6108  rpgt0 6113  ralrp 6119  rpaddcl 6120  rpmulcl 6121  rpdivcl 6122  rpneg 6125  0nrp 6126  expnlbnd 6744  rpsqrcl 6805  absrpcl 6945  clmi2rpi 7178  mulc1cncf 7369  ivthlem2 7372  efcn 7514  cncfmet 7990  lmcvgnns 8028  effoi 8828  ltsubpostb 10709  ltaddpos2tb 10710

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rab 1699  df-v 1859  df-un 2101  df-sn 2464  df-pr 2465  df-op 2468  df-br 2675  df-rp 6106

Copyright terms: Public domain