Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elrp | Unicode version |
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
elrp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 3986 | . 2 | |
2 | df-rp 9590 | . 2 | |
3 | 1, 2 | elrab2 2885 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wcel 2136 class class class wbr 3982 cr 7752 cc0 7753 clt 7933 crp 9589 |
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 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-ext 2147 |
This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-rab 2453 df-v 2728 df-un 3120 df-sn 3582 df-pr 3583 df-op 3585 df-br 3983 df-rp 9590 |
This theorem is referenced by: elrpii 9592 nnrp 9599 rpgt0 9601 rpregt0 9603 ralrp 9611 rexrp 9612 rpaddcl 9613 rpmulcl 9614 rpdivcl 9615 rpgecl 9618 rphalflt 9619 ge0p1rp 9621 rpnegap 9622 negelrp 9623 ltsubrp 9626 ltaddrp 9627 difrp 9628 elrpd 9629 iccdil 9934 icccntr 9936 dfrp2 10199 expgt0 10488 sqrtdiv 10984 mulcn2 11253 ef01bndlem 11697 nconstwlpolem 13943 |
Copyright terms: Public domain | W3C validator |