Theorem elioo2 13441

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 13433	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2848	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5111	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5110	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3648	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1111	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 281	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 290	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  {crab 3414   class class class wbr 5107  (class class class)co 7416  ℝcr 11126  ℝ^*cxr 11269   < clt 11270  (,)cioo 13400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7989  df-2nd 7990  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-ioo 13404

This theorem is used by:  dfrp2  13449  eliooord  13460  elioopnf  13498  elioomnf  13499  difreicc  13539  xov1plusxeqvd  13553  tanhbnd  16253  bl2ioo  25022  xrtgioo  25037  zcld  25044  iccntr  25052  icccmplem2  25054  reconnlem1  25057  reconnlem2  25058  icoopnst  25171  iocopnst  25172  ivthlem3  25685  ovolicc2lem1  25749  ovolicc2lem5  25753  ioombl1lem4  25793  mbfmax  25881  itg2monolem1  25982  itg2monolem3  25984  dvferm1lem  26216  dvferm2lem  26218  dvlip2  26227  dvivthlem1  26240  lhop1lem  26245  lhop  26248  dvcnvrelem1  26249  dvcnvre  26251  itgsubst  26281  sincosq1sgn  26736  sincosq2sgn  26737  sincosq3sgn  26738  sincosq4sgn  26739  coseq00topi  26740  tanabsge  26744  sinq12gt0  26745  sinq12ge0  26746  cosq14gt0  26748  sincos6thpi  26754  sineq0  26762  cos02pilt1  26764  cosq34lt1  26765  cosordlem  26768  cos0pilt1  26770  tanord1  26775  tanord  26776  argregt0  26848  argimgt0  26850  argimlt0  26851  dvloglem  26886  logf1o2  26888  efopnlem2  26895  asinsinlem  27129  acoscos  27131  atanlogsublem  27153  atantan  27161  atanbndlem  27163  atanbnd  27164  atan1  27166  scvxcvx  27223  basellem1  27318  pntibndlem1  27826  pntibnd  27830  pntlemc  27832  padicabvf  27868  padicabvcxp  27869  cnre2csqlem  34422  ivthALT  36956  iooelexlt  38118  itg2gt0cn  38426  iblabsnclem  38434  dvasin  38455  areacirclem1  38459  areacirc  38464  dvrelog3  42933  0nonelalab  42935  cvgdvgrat  45139  radcnvrat  45140  sineq0ALT  45761  ioogtlb  46327  eliood  46330  eliooshift  46338  iooltub  46342  limciccioolb  46453  limcicciooub  46467  cncfioobdlem  46726  ditgeqiooicc  46790  dirkercncflem1  46933  dirkercncflem4  46936  fourierdlem10  46947  fourierdlem32  46969  fourierdlem62  46998  fourierdlem81  47017  fourierdlem82  47018  fourierdlem93  47029  fourierdlem104  47040  fourierdlem111  47047  goldrapos  47750