Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The empty set
vn0
Next ⟩
eq0f
Metamath Proof Explorer
Ascii
Unicode
Theorem
vn0
Description:
The universal class is not equal to the empty set.
(Contributed by
NM
, 11-Sep-2008)
Ref
Expression
Assertion
vn0
⊢
V
≠
∅
Proof
Step
Hyp
Ref
Expression
1
vex
⊢
x
∈
V
2
1
ne0ii
⊢
V
≠
∅