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 13278

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 13270	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2815	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5093	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5092	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3645	. . 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 1541 ∈ wcel 2110 {crab 3393 class class class wbr 5089 (class class class)co 7341 ℝcr 10997 ℝ^*cxr 11137 < clt 11138 (,)cioo 13237

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-pre-lttri 11072 ax-pre-lttrn 11073

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 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 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-po 5522 df-so 5523 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-ov 7344 df-oprab 7345 df-mpo 7346 df-1st 7916 df-2nd 7917 df-er 8617 df-en 8865 df-dom 8866 df-sdom 8867 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-ioo 13241

This theorem is referenced by: dfrp2 13286 eliooord 13297 elioopnf 13335 elioomnf 13336 difreicc 13376 xov1plusxeqvd 13390 tanhbnd 16062 bl2ioo 24700 xrtgioo 24715 zcld 24722 iccntr 24730 icccmplem2 24732 reconnlem1 24735 reconnlem2 24736 icoopnst 24856 iocopnst 24857 ivthlem3 25374 ovolicc2lem1 25438 ovolicc2lem5 25442 ioombl1lem4 25482 mbfmax 25570 itg2monolem1 25671 itg2monolem3 25673 dvferm1lem 25908 dvferm2lem 25910 dvlip2 25920 dvivthlem1 25933 lhop1lem 25938 lhop 25941 dvcnvrelem1 25942 dvcnvre 25944 itgsubst 25976 sincosq1sgn 26427 sincosq2sgn 26428 sincosq3sgn 26429 sincosq4sgn 26430 coseq00topi 26431 tanabsge 26435 sinq12gt0 26436 sinq12ge0 26437 cosq14gt0 26439 sincos6thpi 26445 sineq0 26453 cos02pilt1 26455 cosq34lt1 26456 cosordlem 26459 cos0pilt1 26461 tanord1 26466 tanord 26467 argregt0 26539 argimgt0 26541 argimlt0 26542 dvloglem 26577 logf1o2 26579 efopnlem2 26586 asinsinlem 26821 acoscos 26823 atanlogsublem 26845 atantan 26853 atanbndlem 26855 atanbnd 26856 atan1 26858 scvxcvx 26916 basellem1 27011 pntibndlem1 27520 pntibnd 27524 pntlemc 27526 padicabvf 27562 padicabvcxp 27563 cnre2csqlem 33913 ivthALT 36348 iooelexlt 37375 itg2gt0cn 37694 iblabsnclem 37702 dvasin 37723 areacirclem1 37727 areacirc 37732 dvrelog3 42077 0nonelalab 42079 cvgdvgrat 44325 radcnvrat 44326 sineq0ALT 44948 ioogtlb 45514 eliood 45517 eliooshift 45525 iooltub 45529 limciccioolb 45640 limcicciooub 45654 cncfioobdlem 45913 ditgeqiooicc 45977 dirkercncflem1 46120 dirkercncflem4 46123 fourierdlem10 46134 fourierdlem32 46156 fourierdlem62 46185 fourierdlem81 46204 fourierdlem82 46205 fourierdlem93 46216 fourierdlem104 46227 fourierdlem111 46234

W3C validator