Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The empty set
ne0i
Next ⟩
ne0d
Metamath Proof Explorer
Ascii
Structured
Theorem
ne0i
Description:
If a class has elements, then it is nonempty.
(Contributed by
NM
, 31-Dec-1993)
Ref
Expression
Assertion
ne0i
⊢
(
𝐵
∈
𝐴
→
𝐴
≠ ∅ )
Proof
Step
Hyp
Ref
Expression
1
n0i
⊢
(
𝐵
∈
𝐴
→ ¬
𝐴
= ∅ )
2
1
neqned
⊢
(
𝐵
∈
𝐴
→
𝐴
≠ ∅ )