Metamath Proof Explorer


Theorem elnotel

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

Ref Expression
Assertion elnotel A B ¬ B A

Proof

Step Hyp Ref Expression
1 en2lp ¬ A B B A
2 1 imnani A B ¬ B A