Theorem elioo2 13419

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  {crab 3415   class class class wbr 5108  (class class class)co 7412  ℝcr 11105  ℝ^*cxr 11248   < clt 11249  (,)cioo 13378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180  ax-pre-lttrn 11181

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  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 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-po 5568  df-so 5569  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-ioo 13382

This theorem is used by:  dfrp2  13427  eliooord  13438  elioopnf  13476  elioomnf  13477  difreicc  13517  xov1plusxeqvd  13531  tanhbnd  16223  bl2ioo  24960  xrtgioo  24975  zcld  24982  iccntr  24990  icccmplem2  24992  reconnlem1  24995  reconnlem2  24996  icoopnst  25109  iocopnst  25110  ivthlem3  25623  ovolicc2lem1  25687  ovolicc2lem5  25691  ioombl1lem4  25731  mbfmax  25819  itg2monolem1  25920  itg2monolem3  25922  dvferm1lem  26154  dvferm2lem  26156  dvlip2  26165  dvivthlem1  26178  lhop1lem  26183  lhop  26186  dvcnvrelem1  26187  dvcnvre  26189  itgsubst  26219  sincosq1sgn  26674  sincosq2sgn  26675  sincosq3sgn  26676  sincosq4sgn  26677  coseq00topi  26678  tanabsge  26682  sinq12gt0  26683  sinq12ge0  26684  cosq14gt0  26686  sincos6thpi  26692  sineq0  26700  cos02pilt1  26702  cosq34lt1  26703  cosordlem  26706  cos0pilt1  26708  tanord1  26713  tanord  26714  argregt0  26786  argimgt0  26788  argimlt0  26789  dvloglem  26824  logf1o2  26826  efopnlem2  26833  asinsinlem  27067  acoscos  27069  atanlogsublem  27091  atantan  27099  atanbndlem  27101  atanbnd  27102  atan1  27104  scvxcvx  27161  basellem1  27256  pntibndlem1  27764  pntibnd  27768  pntlemc  27770  padicabvf  27806  padicabvcxp  27807  cnre2csqlem  34309  ivthALT  36874  iooelexlt  38036  itg2gt0cn  38354  iblabsnclem  38362  dvasin  38383  areacirclem1  38387  areacirc  38392  dvrelog3  42860  0nonelalab  42862  cvgdvgrat  45051  radcnvrat  45052  sineq0ALT  45673  ioogtlb  46239  eliood  46242  eliooshift  46250  iooltub  46254  limciccioolb  46365  limcicciooub  46379  cncfioobdlem  46638  ditgeqiooicc  46702  dirkercncflem1  46845  dirkercncflem4  46848  fourierdlem10  46859  fourierdlem32  46881  fourierdlem62  46910  fourierdlem81  46929  fourierdlem82  46930  fourierdlem93  46941  fourierdlem104  46952  fourierdlem111  46959  goldrapos  47648