![]() |
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 4890 | . 2 ⊢ (𝑥 = 𝐴 → (0 < 𝑥 ↔ 0 < 𝐴)) | |
2 | df-rp 12138 | . 2 ⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | |
3 | 1, 2 | elrab2 3576 | 1 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∈ wcel 2107 class class class wbr 4886 ℝcr 10271 0cc0 10272 < clt 10411 ℝ+crp 12137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-br 4887 df-rp 12138 |
This theorem is referenced by: elrpii 12140 nnrp 12150 rpgt0 12151 rpregt0 12153 ralrp 12159 rexrp 12160 rpaddcl 12161 rpmulcl 12162 rpdivcl 12164 rpgecl 12167 rphalflt 12168 ge0p1rp 12170 rpneg 12171 negelrp 12172 ltsubrp 12175 ltaddrp 12176 difrp 12177 elrpd 12178 infmrp1 12486 iccdil 12627 icccntr 12629 1mod 13021 expgt0 13211 resqrex 14398 sqrtdiv 14413 sqrtneglem 14414 mulcn2 14734 ef01bndlem 15316 sinltx 15321 met1stc 22734 met2ndci 22735 bcthlem4 23533 itg2mulc 23951 dvferm1 24185 dvne0 24211 reeff1o 24638 ellogdm 24822 cxpge0 24866 cxple2a 24882 cxpcn3lem 24928 cxpaddlelem 24932 cxpaddle 24933 atanbnd 25104 rlimcnp 25144 amgm 25169 chtub 25389 chebbnd1 25613 chto1ub 25617 pntlem3 25750 blocni 28232 dfrp2 30097 rpdp2cl 30152 dp2ltc 30157 dplti 30175 dpgti 30176 dpexpp1 30178 dpmul4 30184 fdvposlt 31279 hgt750lem 31331 unbdqndv2lem2 33083 heiborlem8 34241 wallispilem4 41212 perfectALTVlem2 42656 regt1loggt0 43345 |
Copyright terms: Public domain | W3C validator |