There is a way in which it is an axiom, and another in which it isn't. I'll try to describe both.
When you do formal logic and start with variables ($x_1,...,x_n,...$), relation symbols ($R_i, i\in I$) and function symbols ($f_j, j\in J$). You build out your formulas with these. An important notion is that of a term in this language. A term is defined recursively as either a variable, or a string of the form $f_j(t_1,...,t_n)$ where $f_j$ is a function symbol of arity $n$ and $t_1,...,t_n$ are terms (this is purely syntactical).
Then you build a deduction system that consists in rules that you may apply in certain situations (for instance if you proved $A$ and $B$, you can prove $A\land B$).
One of these rules is the substitution rule: one way to define it is the following : for any terms $t_1,...,t_n, u_1,...,u_n$ and any function symbol $f$ of arity $n$, if for all $i$, $t_i = u_i$ is proved then one may deduce $f(t_1,...,t_n) = f(u_1,...,u_n)$
In this situation it is an axiom.
However in the common situation of algebra and "the working mathematician", it is a consequence of another substitution rule, the substitution rule for relation symbols. Indeed, all maths can be built from set theory with no function symbol and only one relation symbol ($\in$). In this setting a function $A\to B$ is defined (for instance) as a subset $f$ of $A\times B$ such that for all $x\in A$, there is a unique $b\in B$ such that $(a,b)\in f$. $f(a)$ is then defined as this unique $b$
Now if $x=y \in A$, $f:A\to B$ is a function, then $(x,f(x)) \in f$ and $(y,f(y))\in f$ and so by the substitution rule for relation symbols $(x,f(y))\in f$, so that $f(x)=f(y)$ (by uniqueness).
The substitution rule for relation symbols is very similar to the one for function symbols and is, again an axiom: it can be described as: if $t_1,...,t_n,u_1...,u_n$ are terms, $R$ is a relation symbol of arity $n$; if for all $i$, $t_i= u_i$ has been proved and $R(t_1,...,t_n)$ has been proved, then one may deduce $R(u_1,...,u_n)$
(you may see that the rule is not so far from an axiom, but technically it's not one in this second situation)
f(x) = 1/x
). You need to be careful that both sides of the equation are actually valid "arguments" for your operation. And "do the same" gives you way too many options that aren't valid - e.g. "erase all thex
's" isn't a valid operation, and will break the equality. You might think these are nitpicks, but they are actually serious problems that are at the root of many miscalculations (especially with beginners :) ). $\endgroup$ – Luaan Jun 6 '18 at 6:04