Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
snnzg
Next ⟩
snn0d
Metamath Proof Explorer
Ascii
Unicode
Theorem
snnzg
Description:
The singleton of a set is not empty.
(Contributed by
NM
, 14-Dec-2008)
Ref
Expression
Assertion
snnzg
⊢
A
∈
V
→
A
≠
∅
Proof
Step
Hyp
Ref
Expression
1
snidg
⊢
A
∈
V
→
A
∈
A
2
1
ne0d
⊢
A
∈
V
→
A
≠
∅