This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 → ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( ( 𝐵 ∩ 𝐶 ) ≠ ∅ → 𝐵 = 𝐶 ) ) )

Proof

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