elioo2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elioo2		Structured version Visualization version GIF version

Theorem elioo2 13361

Description: Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)

**Assertion**
Ref	Expression
elioo2	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Proof of Theorem elioo2 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iooval2 13353	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2819	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5151	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5150	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 631	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3682	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1095	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 277	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 286	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 {crab 3432 class class class wbr 5147 (class class class)co 7405 ℝcr 11105 ℝ^*cxr 11243 < clt 11244 (,)cioo 13320

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-pre-lttri 11180 ax-pre-lttrn 11181

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7971 df-2nd 7972 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-ioo 13324

This theorem is referenced by: dfrp2 13369 eliooord 13379 elioopnf 13416 elioomnf 13417 difreicc 13457 xov1plusxeqvd 13471 tanhbnd 16100 bl2ioo 24299 xrtgioo 24313 zcld 24320 iccntr 24328 icccmplem2 24330 reconnlem1 24333 reconnlem2 24334 icoopnst 24446 iocopnst 24447 ivthlem3 24961 ovolicc2lem1 25025 ovolicc2lem5 25029 ioombl1lem4 25069 mbfmax 25157 itg2monolem1 25259 itg2monolem3 25261 dvferm1lem 25492 dvferm2lem 25494 dvlip2 25503 dvivthlem1 25516 lhop1lem 25521 lhop 25524 dvcnvrelem1 25525 dvcnvre 25527 itgsubst 25557 sincosq1sgn 25999 sincosq2sgn 26000 sincosq3sgn 26001 sincosq4sgn 26002 coseq00topi 26003 tanabsge 26007 sinq12gt0 26008 sinq12ge0 26009 cosq14gt0 26011 sincos6thpi 26016 sineq0 26024 cos02pilt1 26026 cosq34lt1 26027 cosordlem 26030 cos0pilt1 26032 tanord1 26037 tanord 26038 argregt0 26109 argimgt0 26111 argimlt0 26112 dvloglem 26147 logf1o2 26149 efopnlem2 26156 asinsinlem 26385 acoscos 26387 atanlogsublem 26409 atantan 26417 atanbndlem 26419 atanbnd 26420 atan1 26422 scvxcvx 26479 basellem1 26574 pntibndlem1 27081 pntibnd 27085 pntlemc 27087 padicabvf 27123 padicabvcxp 27124 cnre2csqlem 32878 ivthALT 35208 iooelexlt 36231 itg2gt0cn 36531 iblabsnclem 36539 dvasin 36560 areacirclem1 36564 areacirc 36569 dvrelog3 40918 0nonelalab 40920 cvgdvgrat 43057 radcnvrat 43058 sineq0ALT 43683 ioogtlb 44194 eliood 44197 eliooshift 44205 iooltub 44209 limciccioolb 44323 limcicciooub 44339 cncfioobdlem 44598 ditgeqiooicc 44662 dirkercncflem1 44805 dirkercncflem4 44808 fourierdlem10 44819 fourierdlem32 44841 fourierdlem62 44870 fourierdlem81 44889 fourierdlem82 44890 fourierdlem93 44901 fourierdlem104 44912 fourierdlem111 44919

W3C validator