Metamath Proof Explorer

Theorem disjne

Description: Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion disjne 
|- ( ( ( A i^i B ) = (/) /\ C e. A /\ D e. B ) -> C =/= D )

Proof

Step Hyp Ref Expression
1 disj 
 |-  ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )
2 eleq1 
 |-  ( x = C -> ( x e. B <-> C e. B ) )
3 2 notbid 
 |-  ( x = C -> ( -. x e. B <-> -. C e. B ) )
4 3 rspccva 
 |-  ( ( A. x e. A -. x e. B /\ C e. A ) -> -. C e. B )
5 eleq1a 
 |-  ( D e. B -> ( C = D -> C e. B ) )
6 5 necon3bd 
 |-  ( D e. B -> ( -. C e. B -> C =/= D ) )
7 4 6 syl5com 
 |-  ( ( A. x e. A -. x e. B /\ C e. A ) -> ( D e. B -> C =/= D ) )
8 1 7 sylanb 
 |-  ( ( ( A i^i B ) = (/) /\ C e. A ) -> ( D e. B -> C =/= D ) )
9 8 3impia 
 |-  ( ( ( A i^i B ) = (/) /\ C e. A /\ D e. B ) -> C =/= D )