Theorem elioo2 13443

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 13435	. . 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 7417  ℝcr 11127  ℝ^*cxr 11270   < clt 11271  (,)cioo 13402

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 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202  ax-pre-lttrn 11203

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 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-ioo 13406

This theorem is used by:  dfrp2  13451  eliooord  13462  elioopnf  13500  elioomnf  13501  difreicc  13541  xov1plusxeqvd  13555  tanhbnd  16255  bl2ioo  25024  xrtgioo  25039  zcld  25046  iccntr  25054  icccmplem2  25056  reconnlem1  25059  reconnlem2  25060  icoopnst  25173  iocopnst  25174  ivthlem3  25687  ovolicc2lem1  25751  ovolicc2lem5  25755  ioombl1lem4  25795  mbfmax  25883  itg2monolem1  25984  itg2monolem3  25986  dvferm1lem  26218  dvferm2lem  26220  dvlip2  26229  dvivthlem1  26242  lhop1lem  26247  lhop  26250  dvcnvrelem1  26251  dvcnvre  26253  itgsubst  26283  sincosq1sgn  26743  sincosq2sgn  26744  sincosq3sgn  26745  sincosq4sgn  26746  coseq00topi  26747  tanabsge  26751  sinq12gt0  26752  sinq12ge0  26753  cosq14gt0  26755  sincos6thpi  26761  sineq0  26769  cos02pilt1  26771  cosq34lt1  26772  cosordlem  26775  cos0pilt1  26777  tanord1  26782  tanord  26783  argregt0  26855  argimgt0  26857  argimlt0  26858  dvloglem  26893  logf1o2  26895  efopnlem2  26902  asinsinlem  27136  acoscos  27138  atanlogsublem  27160  atantan  27168  atanbndlem  27170  atanbnd  27171  atan1  27173  scvxcvx  27230  basellem1  27325  pntibndlem1  27833  pntibnd  27837  pntlemc  27839  padicabvf  27875  padicabvcxp  27876  cnre2csqlem  34428  ivthALT  36962  iooelexlt  38124  itg2gt0cn  38432  iblabsnclem  38440  dvasin  38461  areacirclem1  38465  areacirc  38470  dvrelog3  42939  0nonelalab  42941  cvgdvgrat  45145  radcnvrat  45146  sineq0ALT  45767  ioogtlb  46333  eliood  46336  eliooshift  46344  iooltub  46348  limciccioolb  46459  limcicciooub  46473  cncfioobdlem  46732  ditgeqiooicc  46796  dirkercncflem1  46939  dirkercncflem4  46942  fourierdlem10  46953  fourierdlem32  46975  fourierdlem62  47004  fourierdlem81  47023  fourierdlem82  47024  fourierdlem93  47035  fourierdlem104  47046  fourierdlem111  47053  goldrapos  47756