If that’s it, why is it using ∋ rather than ∈? I would expect “Ǝx∈ℕ”.