![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elioo2 | Structured version Visualization version GIF version |
Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.) |
Ref | Expression |
---|---|
elioo2 | ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iooval2 13357 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}) | |
2 | 1 | eleq2d 2820 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})) |
3 | breq2 5153 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶)) | |
4 | breq1 5152 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵)) | |
5 | 3, 4 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
6 | 5 | elrab 3684 | . . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
7 | 3anass 1096 | . . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) | |
8 | 6, 7 | bitr4i 278 | . 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)) |
9 | 2, 8 | bitrdi 287 | 1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 {crab 3433 class class class wbr 5149 (class class class)co 7409 ℝcr 11109 ℝ*cxr 11247 < clt 11248 (,)cioo 13324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-1st 7975 df-2nd 7976 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-ioo 13328 |
This theorem is referenced by: dfrp2 13373 eliooord 13383 elioopnf 13420 elioomnf 13421 difreicc 13461 xov1plusxeqvd 13475 tanhbnd 16104 bl2ioo 24308 xrtgioo 24322 zcld 24329 iccntr 24337 icccmplem2 24339 reconnlem1 24342 reconnlem2 24343 icoopnst 24455 iocopnst 24456 ivthlem3 24970 ovolicc2lem1 25034 ovolicc2lem5 25038 ioombl1lem4 25078 mbfmax 25166 itg2monolem1 25268 itg2monolem3 25270 dvferm1lem 25501 dvferm2lem 25503 dvlip2 25512 dvivthlem1 25525 lhop1lem 25530 lhop 25533 dvcnvrelem1 25534 dvcnvre 25536 itgsubst 25566 sincosq1sgn 26008 sincosq2sgn 26009 sincosq3sgn 26010 sincosq4sgn 26011 coseq00topi 26012 tanabsge 26016 sinq12gt0 26017 sinq12ge0 26018 cosq14gt0 26020 sincos6thpi 26025 sineq0 26033 cos02pilt1 26035 cosq34lt1 26036 cosordlem 26039 cos0pilt1 26041 tanord1 26046 tanord 26047 argregt0 26118 argimgt0 26120 argimlt0 26121 dvloglem 26156 logf1o2 26158 efopnlem2 26165 asinsinlem 26396 acoscos 26398 atanlogsublem 26420 atantan 26428 atanbndlem 26430 atanbnd 26431 atan1 26433 scvxcvx 26490 basellem1 26585 pntibndlem1 27092 pntibnd 27096 pntlemc 27098 padicabvf 27134 padicabvcxp 27135 cnre2csqlem 32890 ivthALT 35220 iooelexlt 36243 itg2gt0cn 36543 iblabsnclem 36551 dvasin 36572 areacirclem1 36576 areacirc 36581 dvrelog3 40930 0nonelalab 40932 cvgdvgrat 43072 radcnvrat 43073 sineq0ALT 43698 ioogtlb 44208 eliood 44211 eliooshift 44219 iooltub 44223 limciccioolb 44337 limcicciooub 44353 cncfioobdlem 44612 ditgeqiooicc 44676 dirkercncflem1 44819 dirkercncflem4 44822 fourierdlem10 44833 fourierdlem32 44855 fourierdlem62 44884 fourierdlem81 44903 fourierdlem82 44904 fourierdlem93 44915 fourierdlem104 44926 fourierdlem111 44933 |
Copyright terms: Public domain | W3C validator |