Description: A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of TakeutiZaring p. 20. (Contributed by NM, 29-Sep-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | n0 | ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv | ⊢ Ⅎ 𝑥 𝐴 | |
2 | 1 | n0f | ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |