Theorem elioo2 13403

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 13395	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2820	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5123	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5122	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 632	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3671	. . 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 1540   ∈ wcel 2108  {crab 3415   class class class wbr 5119  (class class class)co 7405  ℝcr 11128  ℝ^*cxr 11268   < clt 11269  (,)cioo 13362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-pre-lttri 11203  ax-pre-lttrn 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7988  df-2nd 7989  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-ioo 13366

This theorem is referenced by:  dfrp2  13411  eliooord  13422  elioopnf  13460  elioomnf  13461  difreicc  13501  xov1plusxeqvd  13515  tanhbnd  16179  bl2ioo  24731  xrtgioo  24746  zcld  24753  iccntr  24761  icccmplem2  24763  reconnlem1  24766  reconnlem2  24767  icoopnst  24887  iocopnst  24888  ivthlem3  25406  ovolicc2lem1  25470  ovolicc2lem5  25474  ioombl1lem4  25514  mbfmax  25602  itg2monolem1  25703  itg2monolem3  25705  dvferm1lem  25940  dvferm2lem  25942  dvlip2  25952  dvivthlem1  25965  lhop1lem  25970  lhop  25973  dvcnvrelem1  25974  dvcnvre  25976  itgsubst  26008  sincosq1sgn  26459  sincosq2sgn  26460  sincosq3sgn  26461  sincosq4sgn  26462  coseq00topi  26463  tanabsge  26467  sinq12gt0  26468  sinq12ge0  26469  cosq14gt0  26471  sincos6thpi  26477  sineq0  26485  cos02pilt1  26487  cosq34lt1  26488  cosordlem  26491  cos0pilt1  26493  tanord1  26498  tanord  26499  argregt0  26571  argimgt0  26573  argimlt0  26574  dvloglem  26609  logf1o2  26611  efopnlem2  26618  asinsinlem  26853  acoscos  26855  atanlogsublem  26877  atantan  26885  atanbndlem  26887  atanbnd  26888  atan1  26890  scvxcvx  26948  basellem1  27043  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  padicabvf  27594  padicabvcxp  27595  cnre2csqlem  33941  ivthALT  36353  iooelexlt  37380  itg2gt0cn  37699  iblabsnclem  37707  dvasin  37728  areacirclem1  37732  areacirc  37737  dvrelog3  42078  0nonelalab  42080  cvgdvgrat  44337  radcnvrat  44338  sineq0ALT  44961  ioogtlb  45524  eliood  45527  eliooshift  45535  iooltub  45539  limciccioolb  45650  limcicciooub  45666  cncfioobdlem  45925  ditgeqiooicc  45989  dirkercncflem1  46132  dirkercncflem4  46135  fourierdlem10  46146  fourierdlem32  46168  fourierdlem62  46197  fourierdlem81  46216  fourierdlem82  46217  fourierdlem93  46228  fourierdlem104  46239  fourierdlem111  46246