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

Metamath Proof Explorer

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 )