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 ( 𝐴𝐵 → ¬ 𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 en2lp ¬ ( 𝐴𝐵𝐵𝐴 )
2 1 imnani ( 𝐴𝐵 → ¬ 𝐵𝐴 )