Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Regularity
Introduce the Axiom of Regularity
elneq
Next ⟩
nelaneq
Metamath Proof Explorer
Ascii
Unicode
Theorem
elneq
Description:
A class is not equal to any of its elements.
(Contributed by
AV
, 14-Jun-2022)
Ref
Expression
Assertion
elneq
⊢
A
∈
B
→
A
≠
B
Proof
Step
Hyp
Ref
Expression
1
elirr
⊢
¬
B
∈
B
2
nelelne
⊢
¬
B
∈
B
→
A
∈
B
→
A
≠
B
3
1
2
ax-mp
⊢
A
∈
B
→
A
≠
B