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 13353

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 13345	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2815	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5113	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5112	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3661	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1094	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 278	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 287	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 {crab 3408 class class class wbr 5109 (class class class)co 7389 ℝcr 11073 ℝ^*cxr 11213 < clt 11214 (,)cioo 13312

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 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5253 ax-nul 5263 ax-pow 5322 ax-pr 5389 ax-un 7713 ax-cnex 11130 ax-resscn 11131 ax-pre-lttri 11148 ax-pre-lttrn 11149

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-nul 4299 df-if 4491 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5110 df-opab 5172 df-mpt 5191 df-id 5535 df-po 5548 df-so 5549 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-iota 6466 df-fun 6515 df-fn 6516 df-f 6517 df-f1 6518 df-fo 6519 df-f1o 6520 df-fv 6521 df-ov 7392 df-oprab 7393 df-mpo 7394 df-1st 7970 df-2nd 7971 df-er 8673 df-en 8921 df-dom 8922 df-sdom 8923 df-pnf 11216 df-mnf 11217 df-xr 11218 df-ltxr 11219 df-le 11220 df-ioo 13316

This theorem is referenced by: dfrp2 13361 eliooord 13372 elioopnf 13410 elioomnf 13411 difreicc 13451 xov1plusxeqvd 13465 tanhbnd 16135 bl2ioo 24686 xrtgioo 24701 zcld 24708 iccntr 24716 icccmplem2 24718 reconnlem1 24721 reconnlem2 24722 icoopnst 24842 iocopnst 24843 ivthlem3 25360 ovolicc2lem1 25424 ovolicc2lem5 25428 ioombl1lem4 25468 mbfmax 25556 itg2monolem1 25657 itg2monolem3 25659 dvferm1lem 25894 dvferm2lem 25896 dvlip2 25906 dvivthlem1 25919 lhop1lem 25924 lhop 25927 dvcnvrelem1 25928 dvcnvre 25930 itgsubst 25962 sincosq1sgn 26413 sincosq2sgn 26414 sincosq3sgn 26415 sincosq4sgn 26416 coseq00topi 26417 tanabsge 26421 sinq12gt0 26422 sinq12ge0 26423 cosq14gt0 26425 sincos6thpi 26431 sineq0 26439 cos02pilt1 26441 cosq34lt1 26442 cosordlem 26445 cos0pilt1 26447 tanord1 26452 tanord 26453 argregt0 26525 argimgt0 26527 argimlt0 26528 dvloglem 26563 logf1o2 26565 efopnlem2 26572 asinsinlem 26807 acoscos 26809 atanlogsublem 26831 atantan 26839 atanbndlem 26841 atanbnd 26842 atan1 26844 scvxcvx 26902 basellem1 26997 pntibndlem1 27506 pntibnd 27510 pntlemc 27512 padicabvf 27548 padicabvcxp 27549 cnre2csqlem 33906 ivthALT 36318 iooelexlt 37345 itg2gt0cn 37664 iblabsnclem 37672 dvasin 37693 areacirclem1 37697 areacirc 37702 dvrelog3 42048 0nonelalab 42050 cvgdvgrat 44295 radcnvrat 44296 sineq0ALT 44919 ioogtlb 45486 eliood 45489 eliooshift 45497 iooltub 45501 limciccioolb 45612 limcicciooub 45628 cncfioobdlem 45887 ditgeqiooicc 45951 dirkercncflem1 46094 dirkercncflem4 46097 fourierdlem10 46108 fourierdlem32 46130 fourierdlem62 46159 fourierdlem81 46178 fourierdlem82 46179 fourierdlem93 46190 fourierdlem104 46201 fourierdlem111 46208

W3C validator