The usual approach is to define a concept of a first order language $\mathcal{L}$. They are usually specified by the nonlogical symbols. Well-formed formulas in the language $\mathfrak{L}$ are strings of symbols of $\mathfrak{L}$ along with the logical symbols such as $($, $)$, $\wedge$, $\neg$, variables etc. You can look up in a logic textbook the inductive definition of well-formed formulas, but something like $x \wedge y$ is a well-formed formula, but $(()\neg\wedge xy \neg$ is not a well-formed formula.
A first order theory $T$ in the language $\mathfrak{L}$ is then a collection of well-formed sentences (no free variable) in the language $\mathfrak{L}$. You would then define the deduce relation $T \vdash \varphi$ to mean that there exists a proof of $\varphi$ using $T$. A proof is just a string of of sentences $\phi_1, ..., \phi_n$ such that $\phi_n = \varphi$, each $\phi_i$ is in $T$, a logical axiom of first order logic, follows from modus ponen or generalization using previous $\phi_j$, where $j < i$.
So the above is the definition of a arbitrary first order theory in an arbitrary first order language $\mathfrak{L}$. Now let $\mathfrak{L} = \{\in\}$ a first order language consisting a single binary relation. $ZFC$ is then the first order theory in the language $\mathfrak{L}$ consisting of the "eight axioms" you mentioned above. (Note that ZFC has infinitely may axioms. For example, the axiom schema of specification is actually one axiom for each formula.)
The benefit of this approach where the general definition of first order logic is developed first is that you apply this to study first order logic in general and other first order theories such that the theory of groups, rings, vector space, random graphs, etc. Also first order logic is developed in the metatheory. That is for example, a theorem of ZFC (even if it is about infinite cardinals greater than $\aleph_1$) has a finite proof in the metatheory. However, within ZFC you can formalize first order logic. Then you can consider question about whether $ZFC$ can prove it own consistency.
By taking the approach of developing first order theories in general, you also gain a certain perspective. Some people think that ZFC is something special since it can serve as a foundation for much of mathematics. Through this approach, $ZFC$ is really just another first order theory in a very simple language consisting of a single non-logical symbol. People often have a hard time grasping the idea that $ZFC$ can have different models, for instance one where the continuum hypothesis holds and one where it does not. However, almost everyone would agree that that there exists more than one model of group theory (i.e. more than one group). Sometimes it is helpful to know that results about arbitrary first order theory still apply when one is working in ZFC set theory.
First, you haven't written down the replacement scheme quite correctly. What was probably intended was $$\forall z_1,...,z_n\forall S(\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n,S)\\\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n,S)))$$ (and with a similar modification for the other version).
That aside, the idea you give in your second bullet is a correct argument that the two versions you give are equivalent. In a little more detail, let $z_1,\ldots z_n$ and $S$ be any sets. We need to show $$\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n,S)\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n,S))).$$ Per your idea, consider the an instance of the second version of replacement $$\forall z_1,...,z_{n+1}\forall S(\forall x\in S\exists!y\;\Phi(x,y,z_1,z_2,...,z_n, z_{n+1})\implies\exists R\forall y(y\in R\iff\exists x\in S\;\Phi(x,y,z_1,z_2,...,z_n, z_{n+1}))).$$ and instantiate the outer universal quantifiers as $z_i=z_i$ for $i=1,\ldots n,$ $z_{n+1}$ as $S$ and $S$ as $S,$ and then we have exactly what we needed to show.
Best Answer
There isn't a general algorithm for proving something is not a set. One approach is using a proof by contradiction. Assume it is a set, and derive a contradiction.
Remark: The Class $V = \{x \space| \space x = x\}$ is not a set. Note: We would call V a Proper Class.
I will prove the following claim: "$\{x \space |\space \exists y(x∈y)\}$ is not a set."
Proof by Contradiction:
Assume $A = \{x\space |\space ∃y(x∈y) \}$ is a set (so that we can elicit a contradiction). By Corollary we can find some set $x_0$∉A.
By the Pairing Axiom, since $x_0$ is a set we have that:
$$y = \{x_0,x_0\} = \{x_0\} \space \text{is a set} $$
So, $x_0 \in y$. Thus, the existence of $y$ means that $x_0 \in A$. This is a contradiction as we picked $x_0$ so that it is not in $A$.
Note$_1$: The proof for showing that $\{x \space | \space ∃y(x=y)\}$ is not a set is very similar (Hint: instead of using the Axiom of Pairing, use the Axiom of Extentionality).
Note$_2$: Your intuition about the Axiom of Separation is correct, you could use it directly. The proof would be a more complicated version of using Separation to prove $V$ is a not set.