Description: A class is equal to the empty set if and only if it has no elements. Theorem 2 of Suppes p. 22. (Contributed by NM, 29-Aug-1993)
Ref | Expression | ||
---|---|---|---|
Assertion | eq0 | ⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | ⊢ Ⅎ 𝑥 𝐴 | |
2 | 1 | eq0f | ⊢ ( 𝐴 = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 ) |