Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Regularity
Introduce the Axiom of Regularity
elnotel
Next ⟩
elnel
Metamath Proof Explorer
Ascii
Unicode
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