The extensionality axiom states that sets are the same if they contain the same elements, or conversely, sets are different if there is an element of one that is not an element of the other. This means the element operator $x\in A$ must be a logical function: it does not just produce elements, but must be able to recognize when something is not an element. Question: what is the domain of this function?

Essentially this asks for an a priori way to specify "all possible elements of all sets" in some implementation of the axioms, before defining sets. Worrying about domains is a mathematical thing. If set theory is to provide a foundation for mathematics then it seems to me this question needs a clear, unproblematic answer. Trying to define it in terms of sets or classes is circular. Naive unlimited comprehension is not satisfactory. Philosophical analysis of the question is unhelpful.

Perhaps there is a definition missing, of collections of elements weaker than sets but able to support logical functions. This could also clarify the relationship with categories and homotopy-type-theory. Question: has something like this already been explored?