Theorem disjif

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 30-Dec-2016)

	Ref	Expression
Hypotheses	disjif.1	|- F/_ x C
	disjif.2	|- ( x = Y -> B = C )
Assertion	disjif	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y )

Proof

Step	Hyp	Ref	Expression
1		disjif.1	|- F/_ x C
2		disjif.2	|- ( x = Y -> B = C )
3		inelcm	|- ( ( Z e. B /\ Z e. C ) -> ( B i^i C ) =/= (/) )
4	1 2	disji2f	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ x =/= Y ) -> ( B i^i C ) = (/) )
5	4	3expia	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( x =/= Y -> ( B i^i C ) = (/) ) )
6	5	necon1d	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( ( B i^i C ) =/= (/) -> x = Y ) )
7	6	3impia	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( B i^i C ) =/= (/) ) -> x = Y )
8	3 7	syl3an3	|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y )