Theorem disji

Description: Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D have a common element Z , then X = Y . (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Hypotheses	disji.1	|- ( x = X -> B = C )
	disji.2	|- ( x = Y -> B = D )
Assertion	disji	|- ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) /\ ( Z e. C /\ Z e. D ) ) -> X = Y )

Proof

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