This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )