Theorem elioo2 13397

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 13389	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2811	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5152	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5151	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 630	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3680	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1092	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 277	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 286	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  {crab 3419   class class class wbr 5148  (class class class)co 7417  ℝcr 11137  ℝ^*cxr 11277   < clt 11278  (,)cioo 13356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-pre-lttri 11212  ax-pre-lttrn 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7992  df-2nd 7993  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-ioo 13360

This theorem is referenced by:  dfrp2  13405  eliooord  13415  elioopnf  13452  elioomnf  13453  difreicc  13493  xov1plusxeqvd  13507  tanhbnd  16138  bl2ioo  24739  xrtgioo  24753  zcld  24760  iccntr  24768  icccmplem2  24770  reconnlem1  24773  reconnlem2  24774  icoopnst  24894  iocopnst  24895  ivthlem3  25413  ovolicc2lem1  25477  ovolicc2lem5  25481  ioombl1lem4  25521  mbfmax  25609  itg2monolem1  25711  itg2monolem3  25713  dvferm1lem  25947  dvferm2lem  25949  dvlip2  25959  dvivthlem1  25972  lhop1lem  25977  lhop  25980  dvcnvrelem1  25981  dvcnvre  25983  itgsubst  26015  sincosq1sgn  26464  sincosq2sgn  26465  sincosq3sgn  26466  sincosq4sgn  26467  coseq00topi  26468  tanabsge  26472  sinq12gt0  26473  sinq12ge0  26474  cosq14gt0  26476  sincos6thpi  26481  sineq0  26489  cos02pilt1  26491  cosq34lt1  26492  cosordlem  26495  cos0pilt1  26497  tanord1  26502  tanord  26503  argregt0  26575  argimgt0  26577  argimlt0  26578  dvloglem  26613  logf1o2  26615  efopnlem2  26622  asinsinlem  26854  acoscos  26856  atanlogsublem  26878  atantan  26886  atanbndlem  26888  atanbnd  26889  atan1  26891  scvxcvx  26949  basellem1  27044  pntibndlem1  27553  pntibnd  27557  pntlemc  27559  padicabvf  27595  padicabvcxp  27596  cnre2csqlem  33598  ivthALT  35906  iooelexlt  36928  itg2gt0cn  37235  iblabsnclem  37243  dvasin  37264  areacirclem1  37268  areacirc  37273  dvrelog3  41622  0nonelalab  41624  cvgdvgrat  43832  radcnvrat  43833  sineq0ALT  44458  ioogtlb  44960  eliood  44963  eliooshift  44971  iooltub  44975  limciccioolb  45089  limcicciooub  45105  cncfioobdlem  45364  ditgeqiooicc  45428  dirkercncflem1  45571  dirkercncflem4  45574  fourierdlem10  45585  fourierdlem32  45607  fourierdlem62  45636  fourierdlem81  45655  fourierdlem82  45656  fourierdlem93  45667  fourierdlem104  45678  fourierdlem111  45685