Theorem elioo2 13389

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 13381	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2814	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5146	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5145	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 630	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3680	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1093	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 278	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 287	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  {crab 3427   class class class wbr 5142  (class class class)co 7414  ℝcr 11129  ℝ^*cxr 11269   < clt 11270  (,)cioo 13348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-pre-lttri 11204  ax-pre-lttrn 11205

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-po 5584  df-so 5585  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-er 8718  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 13352

This theorem is referenced by:  dfrp2  13397  eliooord  13407  elioopnf  13444  elioomnf  13445  difreicc  13485  xov1plusxeqvd  13499  tanhbnd  16129  bl2ioo  24695  xrtgioo  24709  zcld  24716  iccntr  24724  icccmplem2  24726  reconnlem1  24729  reconnlem2  24730  icoopnst  24850  iocopnst  24851  ivthlem3  25369  ovolicc2lem1  25433  ovolicc2lem5  25437  ioombl1lem4  25477  mbfmax  25565  itg2monolem1  25667  itg2monolem3  25669  dvferm1lem  25903  dvferm2lem  25905  dvlip2  25915  dvivthlem1  25928  lhop1lem  25933  lhop  25936  dvcnvrelem1  25937  dvcnvre  25939  itgsubst  25971  sincosq1sgn  26420  sincosq2sgn  26421  sincosq3sgn  26422  sincosq4sgn  26423  coseq00topi  26424  tanabsge  26428  sinq12gt0  26429  sinq12ge0  26430  cosq14gt0  26432  sincos6thpi  26437  sineq0  26445  cos02pilt1  26447  cosq34lt1  26448  cosordlem  26451  cos0pilt1  26453  tanord1  26458  tanord  26459  argregt0  26531  argimgt0  26533  argimlt0  26534  dvloglem  26569  logf1o2  26571  efopnlem2  26578  asinsinlem  26810  acoscos  26812  atanlogsublem  26834  atantan  26842  atanbndlem  26844  atanbnd  26845  atan1  26847  scvxcvx  26905  basellem1  27000  pntibndlem1  27509  pntibnd  27513  pntlemc  27515  padicabvf  27551  padicabvcxp  27552  cnre2csqlem  33447  ivthALT  35755  iooelexlt  36777  itg2gt0cn  37083  iblabsnclem  37091  dvasin  37112  areacirclem1  37116  areacirc  37121  dvrelog3  41473  0nonelalab  41475  cvgdvgrat  43673  radcnvrat  43674  sineq0ALT  44299  ioogtlb  44803  eliood  44806  eliooshift  44814  iooltub  44818  limciccioolb  44932  limcicciooub  44948  cncfioobdlem  45207  ditgeqiooicc  45271  dirkercncflem1  45414  dirkercncflem4  45417  fourierdlem10  45428  fourierdlem32  45450  fourierdlem62  45479  fourierdlem81  45498  fourierdlem82  45499  fourierdlem93  45510  fourierdlem104  45521  fourierdlem111  45528