| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > n0 | Structured version Visualization version GIF version | ||
| 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.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| Ref | Expression |
|---|---|
| n0 | ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ne 2941 | . 2 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) | |
| 2 | neq0 4352 | . 2 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
| Copyright terms: Public domain | W3C validator |