![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrp | Structured version Visualization version 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 4791 | . 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴)) | |
2 | df-rp 12037 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
3 | 1, 2 | elrab2 3519 | 1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∈ wcel 2145 class class class wbr 4787 ℝcr 10138 0cc0 10139 < clt 10277 ℝ+crp 12036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-br 4788 df-rp 12037 |
This theorem is referenced by: elrpii 12039 nnrp 12046 rpgt0 12048 rpregt0 12050 ralrp 12056 rexrp 12057 rpaddcl 12058 rpmulcl 12059 rpdivcl 12060 rpgecl 12063 rphalflt 12064 ge0p1rp 12066 rpneg 12067 negelrp 12068 ltsubrp 12070 ltaddrp 12071 difrp 12072 elrpd 12073 infmrp1 12380 iccdil 12518 icccntr 12520 1mod 12911 expgt0 13101 resqrex 14200 sqrtdiv 14215 sqrtneglem 14216 mulcn2 14535 ef01bndlem 15121 sinltx 15126 met1stc 22547 met2ndci 22548 bcthlem4 23344 itg2mulc 23735 dvferm1 23969 dvne0 23995 reeff1o 24422 ellogdm 24607 cxpge0 24651 cxple2a 24667 cxpcn3lem 24710 cxpaddlelem 24714 cxpaddle 24715 atanbnd 24875 rlimcnp 24914 amgm 24939 chtub 25159 chebbnd1 25383 chto1ub 25387 pntlem3 25520 blocni 28001 dfrp2 29873 rpdp2cl 29930 dp2ltc 29935 dplti 29954 dpgti 29955 dpexpp1 29957 dpmul4 29963 fdvposlt 31018 hgt750lem 31070 unbdqndv2lem2 32839 heiborlem8 33950 wallispilem4 40803 perfectALTVlem2 42160 regt1loggt0 42859 |
Copyright terms: Public domain | W3C validator |