Metamath Proof Explorer

Theorem nelelne

Description: Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010) (Proof shortened by AV, 10-May-2020)

Ref Expression
Assertion nelelne ¬ A B C B C A


Step Hyp Ref Expression
1 nelne2 C B ¬ A B C A
2 1 expcom ¬ A B C B C A