Is there a proof that performing an operation on both sides of an equation preserves equality?

In first-order logic, we have the formal substitution principle:

Let $\phi$ be a propositional formula with a free variable $v$, and let $\Gamma$ be a context. Also, let $x, y$ be two terms representing values. Then: \begin{align*} \Gamma & \vdash x = y \\ \Gamma & \vdash \phi[v := x] \\ \hline \Gamma & \vdash \phi[v := y]. \end{align*}

Informally, what this says is: if you can prove in some context that $x=y$, and you can also prove some statement is true for $x$, then you can conclude the same statement is true for $y$. (The notation $\phi[v := x]$ just means the result of substituting $x$ in for $v$ in the proposition formula $\phi$.)

Now, if we are working in a group, let us apply this to the formula $\phi := (a^{-1} (ab) = a^{-1} v)$. Then in the context of the proof, we are assuming $ab = ac$. Also, $\phi[v := ab]$ results in the proposition $a^{-1}(ab) = a^{-1}(ab)$, which is true by the first-order axiom (or in some formulations, the formal proof rule) of reflexivity of equality: $t = t$ for any term $t$. Therefore, the substitution principle allows us to conclude that $\phi[v := ac]$ is true, which results in $a^{-1} (ab) = a^{-1} (ac)$.

To give another application which is implicitly used in the proof, let us see how to use the substitution principle to prove the transitivity of equality: if we have $x=y$ and $y=z$ then $x=z$. For this proof, we will use $\phi := (x = v)$. Then we are assuming $y=z$. We also have that $\phi[v := y]$ is true since it reduces to the assumption $x = y$. Therefore, we can conclude $\phi[v := z]$ which is just $x = z$.

We usually take it as an axiom of the relation of equality. In particular, we assume that on a set $E$ there is a relation $=$ which satisfies the following properties for $a,b,c\in E:$

(1) $a=a$ for all $a\in E$ (egoism), (2) If $a=b,$ then $b=a$ (reciprocity), (3) If $a=b$ and $b=c,$ then $a=c$ (continuity), (4) For any function $f$ defined on $E,$ we have that if $a=b,$ then $f(a)=f(b)$ (conservation).

If the sign "$=$" was some relation that we had just defined on strings like "$ab$", then it would be necessary to establish what you ask for. That is not the case, however. The sign "$=$" denotes equality and juxtaposition of letters denotes multiplication, which is a function. And for every function $f$ you have that $x=y$ implies $f(x)=f(y)$. (Or more similar to the situation here: $x=y$ implies $g(z, x)=g(z, y)$.)