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