Does axiom schema of specification in ZFC states that any sub-set of any set exist? According to axiom schema of specification in ZFC:
$\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 )]$,
where  $\phi$ can be any formula in the language of ZFC with all free variables among $x,z,w_{1},\ldots ,w_{n}$ ($y$ is not free in $\phi$ ).
Informally, the axiom states (as far as I understand) that for any set $z$ there is (exist) a sub-set $y$, if $y$ is constructed in the way described by the axiom schema of specification.
However, couldn't we just say that any subset of set $z$ exist? It looks to me that a set construction provided by the axiom schema of specification works like this: Loop over all elements of the set $z$ check if the current element satisfy condition $\phi$ and, if it is the case, include this element into $y$.
So, couldn't we just write the following?
$\forall z [\forall x ((x \in y) \Rightarrow (x \in z)) \Rightarrow \exists y]$
Moreover, for me it is not clear how this axiom is related to the Power Set Axiom, which states that for any set $A$ there is a set that contains all the subsets of $A$. Shouldn't this axiom (making a statement about a set of all sub-sets) first "prove" that those sub-sets exist?
 A: In standard first-order logic all elements of the universe "exist", so the axiom you've written doesn't really make sense: "$\exists y$" all on its own is not a formula: quantifiers have to govern a predicate, as in $\exists y(y \neq x)$.
However, it is possible to formalise a theory of classes, in which sets like those in ZF feature as a special kind of class. One of the best known systems of this kind is called NBG. In such a system, being a set is a definable property, sets are the things that are elements of some class. So you can define the notion of set-hood thus:
$$
M(x) \equiv \exists y(x \in y)
$$
("M" for "Menge" - German for set.) In such a framework, it is meaningful to write
$$
\forall z\forall y (M(z) \land (\forall x(x \in y \Rightarrow x \in z)) \Rightarrow M(y))
$$
which says that any class $y$ that is contained in a set $z$ is itself a set. This statement or some equivalent statement is one of the axioms of NBG.
A: The string you wrote is not a well-formed string, $$\forall z [\forall x ((x \in y) \Rightarrow (x \in z)) \Rightarrow \exists y]$$
For one, quantifiers can be added to existing formulae, they are not atomic. The goal is to bound a variable into a context. So $\exists y$ on its own is a syntax error. The range of the quantifier is also mishandled, since it leaves the $y$ in the first part free, so you're not even writing an axiom, but rather a formula which requires the assignment to say something meaningful about $y$ in advance.
But maybe it will be clearer if we clarify the terminology. Sets are exactly the things that exist, in the context of $\sf ZFC$, so talking about a sub-set is kind of funny, since it seems to presume the existence from the get go. Every subset of a set $x$ exists, since it's a set by definition. So what's the catch here, why do we even need this axiom?
The axiom of specification is saying that every subclass of a set is a set. In other words, given a set, and given a property, the collection of elements which correspond to the property inside the set will also form a set.
A: The purpose of the axiom schema of specification is to give us a way of writing down (specifying) subsets of a set $z$. That is, for every formula $\phi(x)$, we can construct a subset $\{x\in z\ |\ \phi(x)\}$. In particular every subset of $z$ can be specified by a specific formula.
Without this axiom schema we have no way of knowing how to construct subsets of $z$, let alone showing that they exist. The powerset axiom does not help us either in constructing subsets. The best we could do if we know how to construct a finite number of elements $x_1,\ldots,x_n\in z$ is to construct the finite subset $\{x_1,\ldots,x_n\}\subset z$ with the pairing axiom.
Note that the formula you write is not well formed because you refer to $y$ before it is quantified.
The following question is related: Is the Subset Axiom Schema in ZF necessary?
