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

Proof

Step Hyp Ref Expression
1 elnotel ( 𝐴𝐵 → ¬ 𝐵𝐴 )
2 df-nel ( 𝐵𝐴 ↔ ¬ 𝐵𝐴 )
3 1 2 sylibr ( 𝐴𝐵𝐵𝐴 )