ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elrp Unicode version

Theorem elrp 9395
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
elrp  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )

Proof of Theorem elrp
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 breq2 3901 . 2  |-  ( x  =  A  ->  (
0  <  x  <->  0  <  A ) )
2 df-rp 9394 . 2  |-  RR+  =  { x  e.  RR  |  0  <  x }
31, 2elrab2 2814 1  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    e. wcel 1463   class class class wbr 3897   RRcr 7583   0cc0 7584    < clt 7764   RR+crp 9393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rab 2400  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-br 3898  df-rp 9394
This theorem is referenced by:  elrpii  9396  nnrp  9402  rpgt0  9404  rpregt0  9406  ralrp  9414  rexrp  9415  rpaddcl  9416  rpmulcl  9417  rpdivcl  9418  rpgecl  9421  rphalflt  9422  ge0p1rp  9424  rpnegap  9425  negelrp  9426  ltsubrp  9429  ltaddrp  9430  difrp  9431  elrpd  9432  iccdil  9732  icccntr  9734  expgt0  10277  sqrtdiv  10765  mulcn2  11032  ef01bndlem  11373
  Copyright terms: Public domain W3C validator