I saw this proof in Harvey Friedman notes titled THE AXIOMATIZATION OF SET THEORY BY EXTENSIONALITY, SEPARATION, AND REDUCIBILITY.
This a quote from page 5.
LEMMA 1.2. Let $\varphi$ be a formula in $L(\in)$ whose free variables are among $x_1,…,x_n , n \geq 0$. let $\varphi^W$ be the result of relativizing all quantifiers to $W$. The following is provable in $\sf K(W)$. $$x_1,…,x_n \in W \to (\varphi\leftrightarrow \varphi^W)$$ Proof: By induction on $\varphi$. It suffices to assume this is provable for $\varphi$ and to verify this is provable for $(\exists y)(\varphi)$. Let $x_1,…,x_n $ be such that all free variables of $(\exists y)(\varphi)$ are among $x_1,…,x_n $. Let $\varphi’$ be an alphabetic variant of $\varphi$ (i.e., change in bound variables) in which $x_{n+1}$ does not occur, and consider $\psi = (\exists z)(\varphi’[y/z])$. Then by RED and the induction hypothesis, $$\psi \leftrightarrow (\exists z \in W)(\varphi’[y/z])\leftrightarrow (\exists z \in W)(\varphi’[y/z]^W)\leftrightarrow (\exists z \in W)(\varphi’^W[y/z])\leftrightarrow (\exists y \in W)(\varphi^W)\leftrightarrow (\exists y)(\varphi)^W$$
as required. $\square$
I'm not understanding this proof. For instance $\varphi$ only has its free variables among symbols $x_1,..,x_n$, so it doesn't have the symbol $y$ free. Now the formula $(\exists y)(\varphi)$ doesn't seem to make sense, because $y$ doesn't occur free in $\varphi$.
Also I'm not getting the general plan of the proof? What he's really about to do? Why he is renaming the bound variables?
The theory $\sf K(W)$ Of Friedman is a theory written in first order logic with membership, and a constant symbol $W$. With the following axioms:
Extensionality (EXT): $(\forall z ) (z \in x \leftrightarrow z \in y) \to (\forall z) (x \in z \leftrightarrow y \in z)$
Subworld Separation (SS): $x \in W \to (\exists y \in W)(\forall z)(z \in y \leftrightarrow (z \in x \land \varphi))$, where $\varphi$ is a formula in $L(\in,W)$ in which $y$ is not free.
Reducibility (RED): $(x_1,..,x_n \in W \land \varphi) \to (\exists y \in W)(\varphi)$ where $n \geq 0$, and $\varphi$ is a formula in $L (\in)$, whose free variables are among "$x_1,..,x_n,y$ "