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 13369

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 13361	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2817	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5151	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5150	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 629	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3682	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1093	. . 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 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 {crab 3430 class class class wbr 5147 (class class class)co 7411 ℝcr 11111 ℝ^*cxr 11251 < clt 11252 (,)cioo 13328

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-pre-lttri 11186 ax-pre-lttrn 11187

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 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 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-ioo 13332

This theorem is referenced by: dfrp2 13377 eliooord 13387 elioopnf 13424 elioomnf 13425 difreicc 13465 xov1plusxeqvd 13479 tanhbnd 16108 bl2ioo 24528 xrtgioo 24542 zcld 24549 iccntr 24557 icccmplem2 24559 reconnlem1 24562 reconnlem2 24563 icoopnst 24683 iocopnst 24684 ivthlem3 25202 ovolicc2lem1 25266 ovolicc2lem5 25270 ioombl1lem4 25310 mbfmax 25398 itg2monolem1 25500 itg2monolem3 25502 dvferm1lem 25736 dvferm2lem 25738 dvlip2 25747 dvivthlem1 25760 lhop1lem 25765 lhop 25768 dvcnvrelem1 25769 dvcnvre 25771 itgsubst 25801 sincosq1sgn 26244 sincosq2sgn 26245 sincosq3sgn 26246 sincosq4sgn 26247 coseq00topi 26248 tanabsge 26252 sinq12gt0 26253 sinq12ge0 26254 cosq14gt0 26256 sincos6thpi 26261 sineq0 26269 cos02pilt1 26271 cosq34lt1 26272 cosordlem 26275 cos0pilt1 26277 tanord1 26282 tanord 26283 argregt0 26354 argimgt0 26356 argimlt0 26357 dvloglem 26392 logf1o2 26394 efopnlem2 26401 asinsinlem 26632 acoscos 26634 atanlogsublem 26656 atantan 26664 atanbndlem 26666 atanbnd 26667 atan1 26669 scvxcvx 26726 basellem1 26821 pntibndlem1 27328 pntibnd 27332 pntlemc 27334 padicabvf 27370 padicabvcxp 27371 cnre2csqlem 33188 ivthALT 35523 iooelexlt 36546 itg2gt0cn 36846 iblabsnclem 36854 dvasin 36875 areacirclem1 36879 areacirc 36884 dvrelog3 41236 0nonelalab 41238 cvgdvgrat 43374 radcnvrat 43375 sineq0ALT 44000 ioogtlb 44506 eliood 44509 eliooshift 44517 iooltub 44521 limciccioolb 44635 limcicciooub 44651 cncfioobdlem 44910 ditgeqiooicc 44974 dirkercncflem1 45117 dirkercncflem4 45120 fourierdlem10 45131 fourierdlem32 45153 fourierdlem62 45182 fourierdlem81 45201 fourierdlem82 45202 fourierdlem93 45213 fourierdlem104 45224 fourierdlem111 45231

W3C validator