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 e. B -> -. B e. A )

Proof

Step Hyp Ref Expression
1 en2lp
 |-  -. ( A e. B /\ B e. A )
2 1 imnani
 |-  ( A e. B -> -. B e. A )