Comprehension and Impredicativity Wang and McNaughton (Les Systemes Axiomatiques de la Theorie des Ensembles, 1953) discuss briefly the topic of impredicativity in chapter 2 (titled 'Type Theory') of the above mentioned book, but I'm having difficulty understanding what's going on with a particular example, to which I'll turn immediately after giving you the necessary context.
The context is that of an axiomatic theory T of types, which has three axioms:


*

*$\forall x_i (x_i \in y_{y+1} \leftrightarrow x_i \in z_{i+1}) \rightarrow y_{i+1} = z_{i+1}; \tag{Extensionality}$

*Given $\varphi(x_i)$ s.t. $y_{i+1}$ is not among the free variables of $\varphi$, $$\exists y_{i+1} : \forall x_i(x_i \in y_{i+1} \leftrightarrow \varphi(x_i)) \tag{Comprehension};$$

*A long formula to the effect that there are infinitely many individuals. $\tag{Infinity}$
Toward the very end of that chapter they consider class $w_3$, and claim that this:
$$\forall x_1 : x_i \in y_2 \leftrightarrow \exists z_2(x_1 \in z_2 \land z_2 \in w_3) \tag{4}$$
follows from the axiom of comprehension. If we let
$$\varphi(x_i) := (x_i \in z_{i+1} \land z_{i+1} \in w_3) \tag{5}$$
then it seems that (4) follows from (2). But the definition of comprehension doesn't apply to (4) because (5) defines $\varphi$ in a way that a term of higher-type (viz. $z_{i+1}$) is among the free variables of $\varphi$.
I'm asking, basically, about the legitimacy of the move from axiom (2) to (4) via (5).
 A: I cannot browse Wang & McNaughton' booklet; thus I'll refer to Hao Wang, A Survey of Mathematical Logic (1963), Ch.XVI : DIFFERENT AXIOM SYSTEMS.
See page 406, for an exposition of a "simplified" type theory, following Gödel's 1931 paper.
The "general" restriction is that :

the predicate $\in$ occurs only in contexts of the form $x_n \in y_{i+1}, n = 1, 2, \ldots$. 

The restriction on the axiom of comprehension :

$∃y_{i+1} ∀x_i (x_i \in y_{i+1} ↔ \varphi(x_i))$

is the "standard" one, common also to $\mathsf {ZFC}$, i.e. that $y_{i+1}$ does not occur in $\varphi$.
Thus, the intsance of the formula :

$\varphi(x_i) := \exists z_{i+1} (x_i \in z_{i+1} ∧ z_{i+1} \in w_{i+2})$

used in (4) is :

$\exists z_2 (x_1 \in z_2 ∧ z_2 \in w_3)$

which is well-formed.
When we apply Comprehension to get :


$∀x_1(x_1 \in y_2 ↔ \exists z_2 (x_1 \in z_2 ∧ z_2 \in w_3)$


we have no occurrence of $y_2$ in $\varphi$, which is $\varphi(x_1, w_3)$ ($z_2$ is bound).
The axiom schema of comprehension (or specification) allows for parameters, i.e. free variables $w_i$, different from the $y$.
