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

Oh, doh! I'd missed that.

Yeah, that's...an unusual choice.