Theorem elioo2 13328

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 13320	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2823	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5090	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5089	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 633	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3635	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1095	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 278	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 287	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {crab 3390   class class class wbr 5086  (class class class)co 7358  ℝcr 11026  ℝ^*cxr 11167   < clt 11168  (,)cioo 13287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101  ax-pre-lttrn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-ioo 13291

This theorem is referenced by:  dfrp2  13336  eliooord  13347  elioopnf  13385  elioomnf  13386  difreicc  13426  xov1plusxeqvd  13440  tanhbnd  16117  bl2ioo  24766  xrtgioo  24781  zcld  24788  iccntr  24796  icccmplem2  24798  reconnlem1  24801  reconnlem2  24802  icoopnst  24915  iocopnst  24916  ivthlem3  25429  ovolicc2lem1  25493  ovolicc2lem5  25497  ioombl1lem4  25537  mbfmax  25625  itg2monolem1  25726  itg2monolem3  25728  dvferm1lem  25960  dvferm2lem  25962  dvlip2  25972  dvivthlem1  25985  lhop1lem  25990  lhop  25993  dvcnvrelem1  25994  dvcnvre  25996  itgsubst  26028  sincosq1sgn  26478  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  coseq00topi  26482  tanabsge  26486  sinq12gt0  26487  sinq12ge0  26488  cosq14gt0  26490  sincos6thpi  26496  sineq0  26504  cos02pilt1  26506  cosq34lt1  26507  cosordlem  26510  cos0pilt1  26512  tanord1  26517  tanord  26518  argregt0  26590  argimgt0  26592  argimlt0  26593  dvloglem  26628  logf1o2  26630  efopnlem2  26637  asinsinlem  26872  acoscos  26874  atanlogsublem  26896  atantan  26904  atanbndlem  26906  atanbnd  26907  atan1  26909  scvxcvx  26967  basellem1  27062  pntibndlem1  27571  pntibnd  27575  pntlemc  27577  padicabvf  27613  padicabvcxp  27614  cnre2csqlem  34075  ivthALT  36538  iooelexlt  37689  itg2gt0cn  38007  iblabsnclem  38015  dvasin  38036  areacirclem1  38040  areacirc  38045  dvrelog3  42515  0nonelalab  42517  cvgdvgrat  44755  radcnvrat  44756  sineq0ALT  45378  ioogtlb  45940  eliood  45943  eliooshift  45951  iooltub  45955  limciccioolb  46066  limcicciooub  46080  cncfioobdlem  46339  ditgeqiooicc  46403  dirkercncflem1  46546  dirkercncflem4  46549  fourierdlem10  46560  fourierdlem32  46582  fourierdlem62  46611  fourierdlem81  46630  fourierdlem82  46631  fourierdlem93  46642  fourierdlem104  46653  fourierdlem111  46660