Can we define a set containing all sets within ZFC and then prove that it does not exist? I am currently reading "Elements of Set Theory" by Herbert B. Enderton. The first theorem proven in the book states:

There is no set to which every set belongs.

But isn't it the case that phrase "set to which every set belongs" cannot even be formulated within a theory. According axiom schema of specification (also called the axiom schema of separation or of restricted comprehension) a new set can be defined only using the following formula:
$\forall z \forall w_1 \forall w_2\ldots \forall w_n \exists y \forall x [x \in y \Leftrightarrow (( x \in z )\land \phi )]$
In other words, any new set $y$ can be defined only as a subset of some other set ($z$ in the formula). So, how can we define a set containing all the other sets under this restriction?
So, my concern not about the prove that "set containing all sets" does not exist but about the fact that we prove existence (non-existence) of something that cannot be formulated in terms of the language of theory. It looks like we try to prove within ZFC that "cats" exist. ZFC does not know what is a "cat".
 A: The natural-language statement "there is no set of all sets" is formalized in set theory as $$\neg\exists x\forall y(y\in x),$$ or perhaps more readably $$\forall x\exists y(y\not\in x).$$
(Keep in mind that in $\mathsf{ZFC}$ all things are sets, so "is a set" is just a dummy phrase.)

You seem to be confused about the role of the axioms, e.g. when you write

According axiom schema of specification (also called the axiom schema of separation or of restricted comprehension) a new set can be defined only using the following formula [...].

Axioms are not creative, they are descriptive: they don't in any sense generate the objects that exist, they merely tell us how those objects must behave. The separation axioms don't say that every set has to be created in a certain way, they just describe certain types of set which are guaranteed to exist. And the axioms certainly don't affect what we can define - that's just a language matter, it has nothing to do with the axioms at play.
The following might help:

We can express the property of being a universal set in the language of set theory by the formula $$\upsilon(x):\quad \forall y(y\in x).$$ The $\mathsf{ZFC}$ axioms subsequently imply that no universal set exists, that is, we have $$\mathsf{ZFC}\vdash\forall x\neg\upsilon(x).$$ Different axiom systems may yield different specific results - e.g. the alternative set theory $\mathsf{NFU}$ proves that there is a universal set, and $\mathsf{NFU}$ has strictly weaker consistency strength than $\mathsf{ZFC}$.

A: Noah's answer suffices for ZFC. But even in a foundational system with both sets and non-sets that has axioms similar to ZFC (e.g. ZFA), your argument is still flawed. The sentence "there is no set to which every set belongs" translates obviously and directly to "¬∃S∈Set ∀T∈Set ( T∈S )". Absolutely nothing in this makes any claim about the existence of any set of all sets. Here "Set" denotes a sort, not a set. In fact, the claim is that there does not exist any such set. In simple FOL, quantifiers are unrestricted and range over the entire domain. In many-sorted FOL, each quantifier ranges over a specific sort of objects. For example, a vector space can be easily axiomatized as a 2-sorted structure with one sort for vectors and the other sort for scalars. You can translate many-sorted FOL into simple FOL by using a predicate-symbol for each sort, so the extra expressiveness does not actually matter.
As Noah pointed out, "set to which every set belongs" is a property, not a set, and can be captured in ZFC by a suitable formula with one parameter. I want to point out further that every sentence over a set theory is full of quantifiers over sets in the first place, and there is not even any need to paraphrase any of them to be in terms of properties. For instance, "for every sets $S,T$ there is a set to which an object belongs if and only if it belongs to $S$ or $T$" is a perfectly good sentence using the same kind of phrasing, and you should just translate it using quantifiers.
Also, what Noah means by "set" being a dummy phrase in ZFC is that actually none of the ZFC axioms say anything about "sets". Rather, all of their quantifiers range over the whole (intended) universe. And whatever that universe might be is not actually specified by ZFC. ZFC axiomatizes what some people believe are meaningful FOL statements when the quantifiers are interpreted to range over "sets". (There is in fact a substantial amount of philosophical assumptions underlying some axioms of ZFC.) So the ZFC axioms by themselves are technically meaningless; only after you have interpreted them to be about "sets" do they become statements about "sets". Compare with the FOL theory of groups; none of the axioms say anything about "elements", and they only make sense when you interpret their quantifiers to range over the elements of an actual group and interpret the binary function-symbol to be the actual binary operation in that group.
