Question about a list of ZF axioms and, in particular, SEP In A.G. Hamilton's Logic for mathematicians, eight axioms of ZF are given: EXT, NULL, PAIR, UNION, POW, REP, INF and REG.
The Axiom Scheme of Replacement is formulated like this:
$$
(\forall x_1)(\exists! x_2)\mathscr{A}(x_1,x_2)\to(\forall x_3)(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_3\wedge\mathscr{A}(x_6,x_5)))
$$
My question is:

Since SEP is not taken as an axiom, shouldn't REP be formulated
  $$
(\forall x_1)((\forall x_2)(x_2\in x_1\to(\exists! x_3)\mathscr{A}(x_2,x_3))\to(\exists x_4)(\forall x_5)(x_5\in x_4\leftrightarrow(\exists x_6)(x_6\in x_1\wedge\mathscr{A}(x_6,x_5))))
$$

 A: If I understood your reformulation correctly, you're trying to capture the idea that we must first have a set in order to be able of specifying (or separating) a further set by a property (if that's not the idea, ignore my answer). That "patch", however, is not necessary: the consequent of the axiom already specify that the "values" of the function-like expression must belong to a set in order for there to be a further set containing their "images". Notice that the existential quantifier $\exists x_6$ is dependent on the previous quantifier $\forall x_3$; this means that the consequent states: for every set $x_3$, there is a further set $x_4$ such that for every set $x_5$, $x_5$ is an element of $x_4$ iff there is an element $x_6$ of $x_3$ such that $\mathscr{A}(x_6, x_5)$. 
As for Suppes, note that he's working in a set-theory with urelements (objects which are not sets). That's why he includes a free variable (not bound, as in your case) for sets in his formulation of the axiom.
A: This is confusing. Did you use actual individual variables of the formal language to write the axiom? Or perhaps are $x_1$ to $x_6$ metavariables (metamathematical variables)? If these are individual variables, then this wff is not the REP scheme (without parameters), because the metamathematical variable $\mathscr{A}$ (which represents some wff) has fixed individual variables $x_1$ and $x_2,$ being functional on $x_2$ with $x_1$, and one cannot introduce $x_5$ and $x_6$ in the consequent, except in the case of substitutions of variables (and perhaps this is what you meant whith the brackets "$\mathscr{A}(x_6,x_5)$"), but this is unnecessary. Being $x_1$ to $x_6$ individual variables, of course they are all distinct. Make sure $x_4$ is not free in $\mathscr{A}$ and just repeat $x_2$ and $x_1$ in the consequent like this
$$((\forall x_1)(\exists! x_2) \mathscr{A}) \to (\forall x_3)(\exists x_4)(\forall x_2)((x_2 \in  x_4) \leftrightarrow (\exists x_1)((x_1 \in x_3) \wedge \mathscr{A}))$$
and we are done.
Note that we can interchange the individual variables by others not occurring on the scheme by means of some alphabetic variant (meta)result.
On the other hand, if $x_1$, ..., $x_6$ are metavariables, then one has to make explicit they represent distinct individual variables, except that $x_6$ is $x_1$ and $x_5$ is $x_2$ or they are all distinct and the string $\mathscr{A}(x_6,x_5)$ is the wff obtained from the wff $\mathscr{A}(x_1,x_2)$ by replacing $x_1$ by $x_6$ and $x_2$ by $x_5$ where they are substitutable.
