Consider the string 'Let $y = f(x)$." Suppose that it occurs in some elementary context, such as when graphing the function $f$ using $x$/$y$ coordinates. How is this to be understood in predicate logic? We can't have either $x$ or $y$ be free variables, for consider the following:
Let $f:\mathbb{R}\rightarrow \mathbb{R}, \forall x,\ f(x)=2x$
Let $g:\mathbb{R}→\mathbb{R}, \forall x,\ g(x)=x+x$
Let $y = f(x)$
Let $z = g(x)$
$\therefore y = z$
Here the last line is clearly true, but would lack a truth value if either variable were a free variable.
However, if both variables are bound, we're stuck with permutations of quantifiers that mean the wrong things:
$\forall x,\forall y,y=f(x)$ [says the universe has cardinality 1]
$\forall x,\exists y,y=f(x)$ [says f's domain is the universe]
$\exists y,\forall x,y=f(x)$ [says f is a constant function]
$\exists x,\forall y,y=f(x)$ [says the universe has cardinality 1 and f is nonempty]
$\forall y,\exists x,y=f(x)$ [says f is onto the universe]
$\exists x,\exists y,y=f(x)$ [says f is not the empty function]
It's just a definition of $y$. The statement $y=f(x)$ defines $y$ to be $f(x)$. It doesn't correspond to any particular statement of predicate logic, since you're not claiming anything. Whenever you use $y$ in a statement $P(y)$, you really mean $$\forall y, y=f(x) \implies P(y).$$ You can then use your knowledge that $f$ is a function: $$\exists! y, y = f(x).$$ Using this, you can prove that the extension of the language by adding $y$ is conservative. That means that everything that you prove using this definition of $y$ and does not involve $y$ is actually true even without using $y$. The uniqueness of $y$ guarantees that $f(x) = y$; note that when you say $f(x)$, this is also shorthand for something.
Now to your example. What you're really trying to prove is $$\forall x, \forall y, \forall z, f(x) = y \land g(x) = z \implies y = z. $$ The proof reduces to $x+x=2x$ through the definition of "$f(x)=y$".