Perhaps, your confusion may be resolved by realizing that we do **not** define what a set is using axioms of ZFC. Sets are to us like points are to Euclid. Sets are the primitive objects that we are going to work with.

Let me take a Platonist approach to elaborate. When you set up your axiomatic system, which is ZFC in this case, you assume that there is a universe of objects over which your quantification takes places. (Otherwise, you cannot attach semantics to your system.)

*Sets are simply the objects in the universe. Nothing more, nothing less.* When you include a binary relation symbol $\in$ in the language of your axiomatic system, you assume that between any two objects $x$ and $y$ in your universe, the atomic formula $x \in y$ is either true or false. So, the answer to your question "what is the domain of this function" is: The universe of sets, which is somewhere in the skies!

Whether a sentence such as $\forall x \exists y \neg y \in x$ is true or not is then determined depending on whether for every set $x$ there is a set $y$ such that $x \in y$ holds. Since we do not have direct access to the Platonic universe of sets, we postulate that some statements about the universe of sets are true, which are the axioms of ZFC. Notice that the statement $\emptyset \in \omega$ is not true because we have some kind of function $\cdot \in \omega$ which checks the membership for $\omega$. It is true because it follows from the axioms which posit various facts about the relation $x \in y$.

I admit that I don't fully understand what your problem is. But as you can see, you may give a meaning to all these without circular reasoning. You may also take a formalist approach and simply prove syntactic consequences of the axioms of ZFC without worrying about questions such as "what is a set?" or "what does $x \in y$ mean?".