Metamath Proof Explorer


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 )