Metamath Proof Explorer


Theorem nelne1

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 14-May-2023)

Ref Expression
Assertion nelne1 A B ¬ A C B C

Proof

Step Hyp Ref Expression
1 nelneq2 A B ¬ A C ¬ B = C
2 1 neqned A B ¬ A C B C