Metamath Proof Explorer

Theorem nelneq2

Description: A way of showing two classes are not equal. (Contributed by NM, 12-Jan-2002)

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

Proof

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