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 e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( B e. A /\ C e. A /\ ElDisj A ) -> B e. A )
2		simp2	|- ( ( B e. A /\ C e. A /\ ElDisj A ) -> C e. A )
3		eleq1	|- ( u = B -> ( u e. A <-> B e. A ) )
4		eleq1	|- ( v = C -> ( v e. A <-> C e. A ) )
5	3 4	bi2anan9	|- ( ( u = B /\ v = C ) -> ( ( u e. A /\ v e. A ) <-> ( B e. A /\ C e. A ) ) )
6		ineq12	|- ( ( u = B /\ v = C ) -> ( u i^i v ) = ( B i^i C ) )
7	6	neeq1d	|- ( ( u = B /\ v = C ) -> ( ( u i^i v ) =/= (/) <-> ( B i^i C ) =/= (/) ) )
8		eqeq12	|- ( ( u = B /\ v = C ) -> ( u = v <-> B = C ) )
9	7 8	imbi12d	|- ( ( u = B /\ v = C ) -> ( ( ( u i^i v ) =/= (/) -> u = v ) <-> ( ( B i^i C ) =/= (/) -> B = C ) ) )
10	5 9	imbi12d	|- ( ( u = B /\ v = C ) -> ( ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) <-> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) ) )
11		dfeldisj5a	|- ( ElDisj A <-> A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) )
12		rsp2	|- ( A. u e. A A. v e. A ( ( u i^i v ) =/= (/) -> u = v ) -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
13	11 12	sylbi	|- ( ElDisj A -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
14	13	3ad2ant3	|- ( ( B e. A /\ C e. A /\ ElDisj A ) -> ( ( u e. A /\ v e. A ) -> ( ( u i^i v ) =/= (/) -> u = v ) ) )
15	1 2 10 14	vtocl2d	|- ( ( B e. A /\ C e. A /\ ElDisj A ) -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )
16	15	3expia	|- ( ( B e. A /\ C e. A ) -> ( ElDisj A -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) ) )
17	16	pm2.43b	|- ( ElDisj A -> ( ( B e. A /\ C e. A ) -> ( ( B i^i C ) =/= (/) -> B = C ) ) )