Theorem elioo2 13518

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 13510	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2846	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5106	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5105	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 644	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3644	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1111	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 281	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 290	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {crab 3412   class class class wbr 5102  (class class class)co 7420  ℝcr 11200  ℝ^*cxr 11343   < clt 11344  (,)cioo 13477

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11257  ax-resscn 11258  ax-pre-lttri 11275  ax-pre-lttrn 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-ioo 13481

This theorem is used by:  dfrp2  13526  eliooord  13537  elioopnf  13575  elioomnf  13576  difreicc  13616  xov1plusxeqvd  13630  tanhbnd  16330  bl2ioo  25112  xrtgioo  25127  zcld  25134  iccntr  25142  icccmplem2  25144  reconnlem1  25147  reconnlem2  25148  icoopnst  25261  iocopnst  25262  ivthlem3  25775  ovolicc2lem1  25839  ovolicc2lem5  25843  ioombl1lem4  25883  mbfmax  25971  itg2monolem1  26072  itg2monolem3  26074  dvferm1lem  26305  dvferm2lem  26307  dvlip2  26316  dvivthlem1  26329  lhop1lem  26334  lhop  26337  dvcnvrelem1  26338  dvcnvre  26340  itgsubst  26370  sincosq1sgn  26828  sincosq2sgn  26829  sincosq3sgn  26830  sincosq4sgn  26831  coseq00topi  26832  tanabsge  26836  sinq12gt0  26837  sinq12ge0  26838  cosq14gt0  26840  sincos6thpi  26845  sineq0  26853  cos02pilt1  26855  cosq34lt1  26856  cosordlem  26859  cos0pilt1  26861  tanord1  26866  tanord  26867  argregt0  26939  argimgt0  26941  argimlt0  26942  dvloglem  26977  logf1o2  26979  efopnlem2  26986  asinsinlem  27220  acoscos  27222  atanlogsublem  27244  atantan  27252  atanbndlem  27254  atanbnd  27255  atan1  27257  scvxcvx  27314  basellem1  27409  pntibndlem1  27917  pntibnd  27921  pntlemc  27923  padicabvf  27959  padicabvcxp  27960  cnre2csqlem  34585  ivthALT  37198  iooelexlt  38361  itg2gt0cn  38669  iblabsnclem  38677  dvasin  38698  areacirclem1  38702  areacirc  38707  dvrelog3  43191  0nonelalab  43193  cvgdvgrat  45373  radcnvrat  45374  sineq0ALT  45995  ioogtlb  46583  eliood  46586  eliooshift  46594  iooltub  46598  limciccioolb  46709  limcicciooub  46723  cncfioobdlem  46982  ditgeqiooicc  47046  dirkercncflem1  47189  dirkercncflem4  47192  fourierdlem10  47203  fourierdlem32  47225  fourierdlem62  47254  fourierdlem81  47273  fourierdlem82  47274  fourierdlem93  47285  fourierdlem104  47296  fourierdlem111  47303  goldrapos  48006