Metamath Proof Explorer

Theorem eldisjim3

Description: ElDisj elimination (two chosen elements). Standard specialization lemma: from ElDisj A infer the disjointness condition for two specific elements. (Contributed by Peter Mazsa, 6-Feb-2026)

Ref Expression
Assertion eldisjim3 ⊢ ElDisj A → B ∈ A ∧ C ∈ A → B ∩ C ≠ ∅ → B = C

Proof

Step Hyp Ref Expression
1 simp1 ⊢ B ∈ A ∧ C ∈ A ∧ ElDisj A → B ∈ A
2 simp2 ⊢ B ∈ A ∧ C ∈ A ∧ ElDisj A → C ∈ A
3 eleq1 ⊢ u = B → u ∈ A ↔ B ∈ A
4 eleq1 ⊢ v = C → v ∈ A ↔ C ∈ A
5 3 4 bi2anan9 ⊢ u = B ∧ v = C → u ∈ A ∧ v ∈ A ↔ B ∈ A ∧ C ∈ A
6 ineq12 ⊢ u = B ∧ v = C → u ∩ v = B ∩ C
7 6 neeq1d ⊢ u = B ∧ v = C → u ∩ v ≠ ∅ ↔ B ∩ C ≠ ∅
8 eqeq12 ⊢ u = B ∧ v = C → u = v ↔ B = C
9 7 8 imbi12d ⊢ u = B ∧ v = C → u ∩ v ≠ ∅ → u = v ↔ B ∩ C ≠ ∅ → B = C
10 5 9 imbi12d ⊢ u = B ∧ v = C → u ∈ A ∧ v ∈ A → u ∩ v ≠ ∅ → u = v ↔ B ∈ A ∧ C ∈ A → B ∩ C ≠ ∅ → B = C
11 dfeldisj5a ⊢ ElDisj A ↔ ∀ u ∈ A ∀ v ∈ A u ∩ v ≠ ∅ → u = v
12 rsp2 ⊢ ∀ u ∈ A ∀ v ∈ A u ∩ v ≠ ∅ → u = v → u ∈ A ∧ v ∈ A → u ∩ v ≠ ∅ → u = v
13 11 12 sylbi ⊢ ElDisj A → u ∈ A ∧ v ∈ A → u ∩ v ≠ ∅ → u = v
14 13 3ad2ant3 ⊢ B ∈ A ∧ C ∈ A ∧ ElDisj A → u ∈ A ∧ v ∈ A → u ∩ v ≠ ∅ → u = v
15 1 2 10 14 vtocl2d ⊢ B ∈ A ∧ C ∈ A ∧ ElDisj A → B ∈ A ∧ C ∈ A → B ∩ C ≠ ∅ → B = C
16 15 3expia ⊢ B ∈ A ∧ C ∈ A → ElDisj A → B ∈ A ∧ C ∈ A → B ∩ C ≠ ∅ → B = C
17 16 pm2.43b ⊢ ElDisj A → B ∈ A ∧ C ∈ A → B ∩ C ≠ ∅ → B = C