Theorem elioo2 12810

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 12802	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴(,)𝐵) = {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)})
2	1	eleq2d 2838	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ 𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)}))
3		breq2 5034	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝐴 < 𝑥 ↔ 𝐴 < 𝐶))
4		breq1 5033	. . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 < 𝐵 ↔ 𝐶 < 𝐵))
5	3, 4	anbi12d 634	. . . 4 ⊢ (𝑥 = 𝐶 → ((𝐴 < 𝑥 ∧ 𝑥 < 𝐵) ↔ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
6	5	elrab 3603	. . 3 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
7		3anass 1093	. . 3 ⊢ ((𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵) ↔ (𝐶 ∈ ℝ ∧ (𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))
8	6, 7	bitr4i 281	. 2 ⊢ (𝐶 ∈ {𝑥 ∈ ℝ ∣ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)} ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵))
9	2, 8	bitrdi 290	1 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐶 ∈ (𝐴(,)𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  {crab 3075   class class class wbr 5030  (class class class)co 7148  ℝcr 10564  ℝ^*cxr 10702   < clt 10703  (,)cioo 12769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-pre-lttri 10639  ax-pre-lttrn 10640

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-op 4527  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5428  df-po 5441  df-so 5442  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-ov 7151  df-oprab 7152  df-mpo 7153  df-1st 7691  df-2nd 7692  df-er 8297  df-en 8526  df-dom 8527  df-sdom 8528  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-ioo 12773

This theorem is referenced by:  dfrp2  12818  eliooord  12828  elioopnf  12865  elioomnf  12866  difreicc  12906  xov1plusxeqvd  12920  tanhbnd  15552  bl2ioo  23483  xrtgioo  23497  zcld  23504  iccntr  23512  icccmplem2  23514  reconnlem1  23517  reconnlem2  23518  icoopnst  23630  iocopnst  23631  ivthlem3  24143  ovolicc2lem1  24207  ovolicc2lem5  24211  ioombl1lem4  24251  mbfmax  24339  itg2monolem1  24440  itg2monolem3  24442  dvferm1lem  24673  dvferm2lem  24675  dvlip2  24684  dvivthlem1  24697  lhop1lem  24702  lhop  24705  dvcnvrelem1  24706  dvcnvre  24708  itgsubst  24738  sincosq1sgn  25180  sincosq2sgn  25181  sincosq3sgn  25182  sincosq4sgn  25183  coseq00topi  25184  tanabsge  25188  sinq12gt0  25189  sinq12ge0  25190  cosq14gt0  25192  sincos6thpi  25197  sineq0  25205  cos02pilt1  25207  cosq34lt1  25208  cosordlem  25211  cos0pilt1  25213  tanord1  25218  tanord  25219  argregt0  25290  argimgt0  25292  argimlt0  25293  dvloglem  25328  logf1o2  25330  efopnlem2  25337  asinsinlem  25566  acoscos  25568  atanlogsublem  25590  atantan  25598  atanbndlem  25600  atanbnd  25601  atan1  25603  scvxcvx  25660  basellem1  25755  pntibndlem1  26262  pntibnd  26266  pntlemc  26268  padicabvf  26304  padicabvcxp  26305  cnre2csqlem  31371  ivthALT  34063  iooelexlt  35049  itg2gt0cn  35382  iblabsnclem  35390  dvasin  35411  areacirclem1  35415  areacirc  35420  dvrelog3  39621  0nonelalab  39623  cvgdvgrat  41380  radcnvrat  41381  sineq0ALT  42006  ioogtlb  42488  eliood  42491  eliooshift  42499  iooltub  42503  limciccioolb  42619  limcicciooub  42635  cncfioobdlem  42894  ditgeqiooicc  42958  dirkercncflem1  43101  dirkercncflem4  43104  fourierdlem10  43115  fourierdlem32  43137  fourierdlem62  43166  fourierdlem81  43185  fourierdlem82  43186  fourierdlem93  43197  fourierdlem104  43208  fourierdlem111  43215