Metamath Proof Explorer


Theorem elnel

Description: A class cannot be an element of one of its elements. (Contributed by AV, 14-Jun-2022)

Ref Expression
Assertion elnel A B B A

Proof

Step Hyp Ref Expression
1 elnotel A B ¬ B A
2 df-nel B A ¬ B A
3 1 2 sylibr A B B A