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

Proof

Step Hyp Ref Expression
1 elnotel
 |-  ( A e. B -> -. B e. A )
2 df-nel
 |-  ( B e/ A <-> -. B e. A )
3 1 2 sylibr
 |-  ( A e. B -> B e/ A )