Theorem elioo2 13296

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 13288	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2819	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5099	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5098	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3644	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1094	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 278	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 287	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  {crab 3397   class class class wbr 5095  (class class class)co 7355  ℝcr 11015  ℝ^*cxr 11155   < clt 11156  (,)cioo 13255

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11072  ax-resscn 11073  ax-pre-lttri 11090  ax-pre-lttrn 11091

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 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-1st 7930  df-2nd 7931  df-er 8631  df-en 8879  df-dom 8880  df-sdom 8881  df-pnf 11158  df-mnf 11159  df-xr 11160  df-ltxr 11161  df-le 11162  df-ioo 13259

This theorem is referenced by:  dfrp2  13304  eliooord  13315  elioopnf  13353  elioomnf  13354  difreicc  13394  xov1plusxeqvd  13408  tanhbnd  16080  bl2ioo  24717  xrtgioo  24732  zcld  24739  iccntr  24747  icccmplem2  24749  reconnlem1  24752  reconnlem2  24753  icoopnst  24873  iocopnst  24874  ivthlem3  25391  ovolicc2lem1  25455  ovolicc2lem5  25459  ioombl1lem4  25499  mbfmax  25587  itg2monolem1  25688  itg2monolem3  25690  dvferm1lem  25925  dvferm2lem  25927  dvlip2  25937  dvivthlem1  25950  lhop1lem  25955  lhop  25958  dvcnvrelem1  25959  dvcnvre  25961  itgsubst  25993  sincosq1sgn  26444  sincosq2sgn  26445  sincosq3sgn  26446  sincosq4sgn  26447  coseq00topi  26448  tanabsge  26452  sinq12gt0  26453  sinq12ge0  26454  cosq14gt0  26456  sincos6thpi  26462  sineq0  26470  cos02pilt1  26472  cosq34lt1  26473  cosordlem  26476  cos0pilt1  26478  tanord1  26483  tanord  26484  argregt0  26556  argimgt0  26558  argimlt0  26559  dvloglem  26594  logf1o2  26596  efopnlem2  26603  asinsinlem  26838  acoscos  26840  atanlogsublem  26862  atantan  26870  atanbndlem  26872  atanbnd  26873  atan1  26875  scvxcvx  26933  basellem1  27028  pntibndlem1  27537  pntibnd  27541  pntlemc  27543  padicabvf  27579  padicabvcxp  27580  cnre2csqlem  33934  ivthALT  36390  iooelexlt  37417  itg2gt0cn  37725  iblabsnclem  37733  dvasin  37754  areacirclem1  37758  areacirc  37763  dvrelog3  42168  0nonelalab  42170  cvgdvgrat  44420  radcnvrat  44421  sineq0ALT  45043  ioogtlb  45609  eliood  45612  eliooshift  45620  iooltub  45624  limciccioolb  45735  limcicciooub  45749  cncfioobdlem  46008  ditgeqiooicc  46072  dirkercncflem1  46215  dirkercncflem4  46218  fourierdlem10  46229  fourierdlem32  46251  fourierdlem62  46280  fourierdlem81  46299  fourierdlem82  46300  fourierdlem93  46311  fourierdlem104  46322  fourierdlem111  46329