This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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