How to prove this sequent in first-order logic?

Question

Let $\Sigma$ be a signature and $\phi$ be a formula over $\Sigma$ and $\vec{y}$ be a context suitable for it. How do I show that the following sequent is derivable? namely

$$\phi\!\left[\vec{x}\!\left/\vec{y}\right.\right]\vdash_{\vec{x}}\left(\exists \vec{y}\right)\left(\phi\land\left(\vec{y} = \vec{x}\right)\right)$$

It feels trivial but I don't find any suitable rules to derive it. For reference by rules I mean the following (I just don't find anything that allows me to deduct a sequent containing $\exists y$ that appears on the right of $\vdash$):

Answer 1

Rewritten after h__'s comment

1) $(∃y)(\phi \land (y=x)) ⊢_x (∃y)(\phi \land (y=x))$ --- identity axiom

2) $\phi \land (y=x) ⊢_{x,y} (∃y)(\phi \land (y=x))$ --- rule for existential quantification

3) $\phi[x/y] \land (x=x) ⊢_x (∃y)(\phi \land (y=x))$ --- with substitution $[x/y]$.

4) $\phi[x/y] \vdash_x \phi[x/y]$ --- identity axiom

5) $\phi[x/y] \vdash_x \top$ --- rule for (finite) conjunction

6) $\top \vdash_x (x=x)$ --- equality rule

7) $\phi[x/y] \vdash_x (x=x)$ --- from 5) and 6) by cut rule

8) $\phi[x/y] \vdash \phi[x/y] \land (x=x)$ --- from 4) and 7) by rule for (finite) conjunction

$\phi[x/y] \vdash_x (∃y)(\phi \land (y=x))$ --- from 3) and 8) by cut rule.