When I was teaching predicate calculus in the introductory course last semester (Well, I was a TA but still...) we took the following approach:
Define terms and formulae.
A term is practically a name for some element of the interpretation (the structure), either a free variable, or a constant in the language and if $F$ is a function and $t_1,\ldots ,t_k$ are terms then $F(t_1,\ldots ,t_k)$ is also a term.
On the other hand, formulae have the familiar structure. You start with atomic formulae which are relations (either equality or within the language) and terms and you say that if you have two formulae then the conjugation, disjunction, negation and implication give you a new formula, as well quantification of $\exists$ and $\forall$.
So the formula $\varphi(x,y)\colon = y=f(x)$ is a formula which receives a TRUE value whenever $y$ is assigned to be $f^M(x)$, it is an atomic formula - namely the equality of two terms.
Now considering the $f$ and $g$ that you have presented above. You will need to have $2$ as a constant in your language, as well the functions of multiplication and addition. Then you want to require your structure to satisfy the axioms that $x+x = 2x$, namely the usual ring axioms (well, you want $\mathbb{R}$ to behave normally) and then you can deduce that.
The lines "let $y = f(x)$" and "let $z=g(x)$" then "$z=y$" can be formulated as follow:
$$\forall x\forall y\forall z((y=f(x) \wedge z=g(x))\rightarrow z=y)$$
Or more explicitly:
$$\forall x\forall y\forall z((y=2\cdot x\wedge z=x+x)\rightarrow z=y)$$
Addendum:
Another way to look at that is that by definibility. Your language has the addition and multiplication, and $0$, and $1$ as constants.
With that you can define a formula $\varphi(x,y)$ which is only satisfied when $y=f(x)$. In this sense, we have enriched the language with new function symbols - $f$ and $g$.
Now when you say "let $y=f(x)$ and $z=g(x)$" you enrich the language with three other constants, named $x,y,z$, and you add an axiom to you theory "$y=f(x)$" and "$z=g(x)$". Now you claim that from your theory you can deduce that the new constants $y$ and $z$ are interpreted as the same element in the structure.