Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
snidb
Next ⟩
snid
Metamath Proof Explorer
Ascii
Unicode
Theorem
snidb
Description:
A class is a set iff it is a member of its singleton.
(Contributed by
NM
, 5-Apr-2004)
Ref
Expression
Assertion
snidb
⊢
A
∈
V
↔
A
∈
A
Proof
Step
Hyp
Ref
Expression
1
snidg
⊢
A
∈
V
→
A
∈
A
2
elex
⊢
A
∈
A
→
A
∈
V
3
1
2
impbii
⊢
A
∈
V
↔
A
∈
A