Metamath Proof Explorer

Theorem nelneq

Description: A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997)

Ref Expression
Assertion nelneq 
|- ( ( A e. C /\ -. B e. C ) -> -. A = B )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = B -> ( A e. C <-> B e. C ) )
2 1 biimpcd 
 |-  ( A e. C -> ( A = B -> B e. C ) )
3 2 con3dimp 
 |-  ( ( A e. C /\ -. B e. C ) -> -. A = B )