Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Regularity
Introduce the Axiom of Regularity
elnel
Next ⟩
en3lplem1
Metamath Proof Explorer
Ascii
Unicode
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
∈
B
→
B
∉
A
Proof
Step
Hyp
Ref
Expression
1
elnotel
⊢
A
∈
B
→
¬
B
∈
A
2
df-nel
⊢
B
∉
A
↔
¬
B
∈
A
3
1
2
sylibr
⊢
A
∈
B
→
B
∉
A