This answer pertains to the system presented here, which is a relatively typical Hilbert-style system.
First, you cannot use a simple substitution. By definition, a substitution only replaces free variables. So if you try to substitute $y$ for $x$ in $(\exists x)\phi(x)$ you get back the same formula $(\exists x)\phi(x)$. This is a very common convention, and is not at all unique to this author.
To prove in this author's particular system that $(\exists x)\phi(x)$ implies $(\exists y)\phi(y)$, where $y$ is admissible for $x$ in $\phi$, you can use rule $L_{15}$ in the following form: $ (\forall x)[\phi(x) \to (\exists y)\phi(y)] \to [(\exists x)\phi(x) \to (\exists y)\phi(y)] $ This is a correct instance of $L_{15}$ because in $(\exists y)\phi(y)$ all the free occurrences of $x$ in $\phi(x)$ were replaced with $y$, so $x$ is not free in $(\exists y)\phi(y)$. Now the problem is to show that the hypothesis $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$ can be deduced, because then the conclusion $(\exists x)\phi(x) \to (\exists y)\phi(y)$ follows immediately by modus ponens.
To prove $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$, first, use rule $L_{13}$ to obtain $\phi(x) \to (\exists y)\phi(y)$. This is a correct instance of $L_{13}$ because $y$ is admissible for $x$. Now use the generalization rule from page 6 to obtain $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$.
Many proof systems have a separate rule of inference, called existential instantiation, which says that from $(\exists x)\phi(x)$ you can deduce $\phi(z)$ where $z$ is chosen as a new variable that has not yet appeared at all in the proof. In such a system, the deduction would go as follows, in symbolic form: $ (\exists x)\phi(x) \Longrightarrow \phi(z) \Longrightarrow (\exists y)\phi(y) $ where the second $\Longrightarrow$ uses rule $L_{13}$, which works because $z$ was chosen in such a way to guarantee it was admissible for $x$.
The proof system adopted by this author does not directly admit this rule, but it is straightforward to make it work by Skolemization: add a new constant symbol $z_\phi$ to your language and add a logical axiom $(\forall x)[\phi(x) \to \phi(z_\phi)]$. Thus $z_\phi$ will be an element such that if any element satisfies $\phi$ then $z_\phi$ does. This axiom does not affect the consistency of any theory to which it is added, because any structure for the original theory can be expanded in such a way that the new logical axiom is true, and any structure in which the enlarged system holds automatically satisfies the original system, just by ignoring $z_\phi$. Therefore, using this and the completeness theorems for the original and expanded systems, a sentence in the original language is provable in the original system if and only if it is provable in the expanded system.
Now existential instantiation is an immediate consequence of $L_{15}$ and the new axiom for $z_\phi$ described in the previous paragraph. As a historical note, Hilbert developed a very similar idea which goes by the name $\epsilon$ calculus. What I call $z_\phi$ woulc be called $(\epsilon x)\phi(x)$ in that system.
The way that I look at the proof I described above in the original system is that it is a simulation of existential instantiation that just avoids directly using the rule for $z_\phi$ or the $\epsilon$ operator. The cost of avoiding them is that the other axioms have to be used in less obvious ways. Informally, $ (\forall a)[\phi(a) \to \psi] \to [(\exists x) \phi(x) \to \psi] $ says that if we can prove $\phi(a) \to \psi$ for a suitable variable $a$, then we could have proved $(\exists x)\phi(x) \to \psi$. So in other words if we want to prove the latter it is enough to pick a suitable $a$ and prove the former. This is analogous to what the existential instantiation rule says: given $(\exists x)\phi(x)$ we should try working with $\phi(a)$ instead.