![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elrp | GIF version |
Description: Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
Ref | Expression |
---|---|
elrp | ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq2 3871 | . 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴)) | |
2 | df-rp 9234 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
3 | 1, 2 | elrab2 2788 | 1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∈ wcel 1445 class class class wbr 3867 ℝcr 7446 0cc0 7447 < clt 7619 ℝ+crp 9233 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rab 2379 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 df-br 3868 df-rp 9234 |
This theorem is referenced by: elrpii 9236 nnrp 9242 rpgt0 9244 rpregt0 9246 ralrp 9254 rexrp 9255 rpaddcl 9256 rpmulcl 9257 rpdivcl 9258 rpgecl 9261 rphalflt 9262 ge0p1rp 9264 rpnegap 9265 ltsubrp 9267 ltaddrp 9268 difrp 9269 elrpd 9270 iccdil 9564 icccntr 9566 expgt0 10119 sqrtdiv 10606 mulcn2 10871 ef01bndlem 11211 |
Copyright terms: Public domain | W3C validator |