Thank you both Stephan and FL. That Math Exchange link was particularly useful.
So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set (I've read the definition in Specifying Systems). In practice, however, it seems like this can always be avoided, and rather trivially. I have heard people dismiss TLA+ as "not even higher-order (like Coq)", and so less expressive. Similarly, I've heard people say that things like separation logic require higher-orderness, but from what little I've seen of it (which is very little), it also seems to be rather trivially expressed in TLA+. Is there an actual difference in expressiveness or just a formal one?
Ron