Theorem elioo2 13412

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 13404	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2847	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5112	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5111	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 643	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3649	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1109	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 281	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 290	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141  {crab 3414   class class class wbr 5108  (class class class)co 7410  ℝcr 11098  ℝ^*cxr 11241   < clt 11242  (,)cioo 13371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11155  ax-resscn 11156  ax-pre-lttri 11173  ax-pre-lttrn 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7985  df-2nd 7986  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-ioo 13375

This theorem is referenced by:  dfrp2  13420  eliooord  13431  elioopnf  13469  elioomnf  13470  difreicc  13510  xov1plusxeqvd  13524  tanhbnd  16216  bl2ioo  24928  xrtgioo  24943  zcld  24950  iccntr  24958  icccmplem2  24960  reconnlem1  24963  reconnlem2  24964  icoopnst  25077  iocopnst  25078  ivthlem3  25591  ovolicc2lem1  25655  ovolicc2lem5  25659  ioombl1lem4  25699  mbfmax  25787  itg2monolem1  25888  itg2monolem3  25890  dvferm1lem  26122  dvferm2lem  26124  dvlip2  26133  dvivthlem1  26146  lhop1lem  26151  lhop  26154  dvcnvrelem1  26155  dvcnvre  26157  itgsubst  26187  sincosq1sgn  26639  sincosq2sgn  26640  sincosq3sgn  26641  sincosq4sgn  26642  coseq00topi  26643  tanabsge  26647  sinq12gt0  26648  sinq12ge0  26649  cosq14gt0  26651  sincos6thpi  26657  sineq0  26665  cos02pilt1  26667  cosq34lt1  26668  cosordlem  26671  cos0pilt1  26673  tanord1  26678  tanord  26679  argregt0  26751  argimgt0  26753  argimlt0  26754  dvloglem  26789  logf1o2  26791  efopnlem2  26798  asinsinlem  27032  acoscos  27034  atanlogsublem  27056  atantan  27064  atanbndlem  27066  atanbnd  27067  atan1  27069  scvxcvx  27126  basellem1  27221  pntibndlem1  27729  pntibnd  27733  pntlemc  27735  padicabvf  27771  padicabvcxp  27772  cnre2csqlem  34266  ivthALT  36812  iooelexlt  37974  itg2gt0cn  38292  iblabsnclem  38300  dvasin  38321  areacirclem1  38325  areacirc  38330  dvrelog3  42800  0nonelalab  42802  cvgdvgrat  44993  radcnvrat  44994  sineq0ALT  45615  ioogtlb  46181  eliood  46184  eliooshift  46192  iooltub  46196  limciccioolb  46307  limcicciooub  46321  cncfioobdlem  46580  ditgeqiooicc  46644  dirkercncflem1  46787  dirkercncflem4  46790  fourierdlem10  46801  fourierdlem32  46823  fourierdlem62  46852  fourierdlem81  46871  fourierdlem82  46872  fourierdlem93  46883  fourierdlem104  46894  fourierdlem111  46901  goldrapos  47587