Metamath Proof Explorer

Theorem elnelne2

Description: Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020)

Ref Expression
Assertion elnelne2 A C B C A B


Step Hyp Ref Expression
1 df-nel B C ¬ B C
2 nelne2 A C ¬ B C A B
3 1 2 sylan2b A C B C A B