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 13314

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 13306	. . 3 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2823	. 2 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5104	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5103	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3648	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1095	. . 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 1087 = wceq 1542 ∈ wcel 2114 {crab 3401 class class class wbr 5100 (class class class)co 7368 ℝcr 11037 ℝ^*cxr 11177 < clt 11178 (,)cioo 13273

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-pre-lttri 11112 ax-pre-lttrn 11113

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-po 5540 df-so 5541 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-1st 7943 df-2nd 7944 df-er 8645 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-ioo 13277

This theorem is referenced by: dfrp2 13322 eliooord 13333 elioopnf 13371 elioomnf 13372 difreicc 13412 xov1plusxeqvd 13426 tanhbnd 16098 bl2ioo 24748 xrtgioo 24763 zcld 24770 iccntr 24778 icccmplem2 24780 reconnlem1 24783 reconnlem2 24784 icoopnst 24904 iocopnst 24905 ivthlem3 25422 ovolicc2lem1 25486 ovolicc2lem5 25490 ioombl1lem4 25530 mbfmax 25618 itg2monolem1 25719 itg2monolem3 25721 dvferm1lem 25956 dvferm2lem 25958 dvlip2 25968 dvivthlem1 25981 lhop1lem 25986 lhop 25989 dvcnvrelem1 25990 dvcnvre 25992 itgsubst 26024 sincosq1sgn 26475 sincosq2sgn 26476 sincosq3sgn 26477 sincosq4sgn 26478 coseq00topi 26479 tanabsge 26483 sinq12gt0 26484 sinq12ge0 26485 cosq14gt0 26487 sincos6thpi 26493 sineq0 26501 cos02pilt1 26503 cosq34lt1 26504 cosordlem 26507 cos0pilt1 26509 tanord1 26514 tanord 26515 argregt0 26587 argimgt0 26589 argimlt0 26590 dvloglem 26625 logf1o2 26627 efopnlem2 26634 asinsinlem 26869 acoscos 26871 atanlogsublem 26893 atantan 26901 atanbndlem 26903 atanbnd 26904 atan1 26906 scvxcvx 26964 basellem1 27059 pntibndlem1 27568 pntibnd 27572 pntlemc 27574 padicabvf 27610 padicabvcxp 27611 cnre2csqlem 34087 ivthALT 36548 iooelexlt 37606 itg2gt0cn 37915 iblabsnclem 37923 dvasin 37944 areacirclem1 37948 areacirc 37953 dvrelog3 42424 0nonelalab 42426 cvgdvgrat 44658 radcnvrat 44659 sineq0ALT 45281 ioogtlb 45844 eliood 45847 eliooshift 45855 iooltub 45859 limciccioolb 45970 limcicciooub 45984 cncfioobdlem 46243 ditgeqiooicc 46307 dirkercncflem1 46450 dirkercncflem4 46453 fourierdlem10 46464 fourierdlem32 46486 fourierdlem62 46515 fourierdlem81 46534 fourierdlem82 46535 fourierdlem93 46546 fourierdlem104 46557 fourierdlem111 46564

W3C validator