Why do the axioms of equality suffice? In this answer, Henning Makholm axiomatizes the notion of equality as follows:
Reflexive axiom, Symmetry axiom and Transitive axiom:

The properties we need are the pure equality axioms:
  
  
*
  
*$x=x$
  
*$x=y ⇒ y=x$
  
*$x=y∧y=z ⇒ x=z$ [...]
  

Substitution axiom (scheme):

plus the crucial property that we're allowed to substitute equals for equals in an expression and not change the meaning:
  $x=y⇒f(x)=f(y)$.

He then makes this comment on this latter axiom:

[The substitution axiom] is a bit tricky to express formally because we don't yet have the machinery to speak about arbitrary functions (and developing this machinery generally depends on having equality working already). So what one does instead is to have a whole slew of axioms for each primitive operation in our theory:
$$x=y \Rightarrow x+z=y+z \qquad x=y \Rightarrow z+x=z+y \\
x=y \Rightarrow x\times z=y\times z \qquad x=y \Rightarrow z\times x=z\times y \\
x=y \Rightarrow -x = -y \\
x=y \Rightarrow (x<z \Leftrightarrow y<z) \qquad
x=y \Rightarrow (z<x \Leftrightarrow z<y)$$
  and so forth. And each time we add a new operator or relation symbol this kind of equality rules should also be added for it.


My question is:
How can one ensure that the given axioms of equality (Reflexive axiom, Symmetry axiom, Transitive axiom, Substitution axiom) suffice to deduce all other evident statements about equality?
 A: First, we have to make the question precise. The version I'll use is the following (here $\mathsf{FOL_{w/o=}}$ is first-order logic without equality, and $\equiv_{\mathsf{w/o=}}$ is the elementary equivalence relation for first-order logic without equality):

A set of rules $\mathbb{S}$ captures the first-order behavior of equality iff whenever $\mathcal{A}$ is a structure and $E$ is an equivalence relation on $\mathcal{A}$ satisfying all the rules in $\mathbb{S}$ as far as $\mathcal{A}$ is concerned - e.g. in the case of the ruleset of the OP, we need among other things that $$(\mathcal{A},E)\models aEb\rightarrow f(a)Ef(b)$$ for each unary function symbol $f$ in the signature of $\mathcal{A}$ - there is some structure $\mathcal{B}$ such that $(\mathcal{A},E)\equiv_{\mathsf{w/o=}}(\mathcal{B}, =)$.

The intuition behind this is the following. Suppose $\varphi$ is some $\mathsf{FOL_{w/o=}}$ sentence which is true of equality in every structure; we want to show that if $\mathbb{S}$ has the property above and $E$ satisfies $\mathbb{S}$ in $\mathcal{A}$, then $(\mathcal{A},E)$ also satisfies $\varphi$. Let $\mathcal{B}$ be as guaranteed by the hypothesis on $\mathbb{S}$; then $(\mathcal{B},=)\models\varphi$ by our assumption on $\varphi$, so $(\mathcal{A},E)\models\varphi$ since $(\mathcal{A},E)\equiv(\mathcal{B},=)$.
(We could also have made do with a weaker condition: say that $\mathbb{S}$ weakly captures the first-order behavior of equality iff for every $\mathsf{FOL_{w/o=}}$ sentence $\varphi$, if $E$ is an equivalence relation on a structure $\mathcal{A}$ which satisfies all the rules in $\mathbb{S}$ then there is some structure $\mathcal{B}_\varphi$ such that $(\mathcal{A},E)\models\varphi\iff(\mathcal{B},=)\models\varphi$. But this seems less natural to me.)
The idea behind proving that the set of rules above (with a crucial elaboration - see below) captures the first-order behavior of equality is as follows. Suppose $E$ is an equivalence relation on a structure $\mathcal{A}$ satisfying all of those rules. Then $E$ is a congruence on $\mathcal{A}$, and so we can form the quotient structure $\mathcal{B}:=\mathcal{A}/E$. We then want to argue that $(\mathcal{A},E)\equiv_{\mathsf{w/o=}}(\mathcal{B},=)$.
The elaboration on the rule set in the OP mentioned in the previous paragraph is the following: we need substitution for all $\mathsf{FOL_{w/o=}}$ formulas, not just atomic ones. That is, if an equivalence relation $E$ on a structure $\mathcal{A}$ is to satisfy our strong substitution rule we need $$a_1Eb_1,...,a_nEb_n\implies \mathcal{A}\models\theta(a_1,...,a_n)\leftrightarrow\theta(b_1,...,b_n)$$ for each $\mathsf{FOL_{w/o=}}$-formula $\theta(x_1,...,x_n)$. This stronger substitution rule makes the argument hoped for by the last sentence in the previous paragraph basically immediate; meanwhile, it's a good exercise to show that merely being a congruence is not enough to capture the first-order behavior of equality (think about e.g. a nonabelian group with an abelian quotient).

However, there is an interesting subtlety here. There are logics besides first-order logic, and the equality rules in the OP (with the strong form of substitution) can be naturally generalized to any such logic. We can then ask whether the sufficiency result above generalizes to any "reasonable logical system" $\mathfrak{L}$. Interestingly, the answer is that it sometimes but not always generalizes.
Suppose I have a "reasonable logical system" $\mathfrak{L}$ (e.g. first-order logic, second-order logic, infinitary logic(s), ...). For a structure $\mathcal{A}$ and a binary relation $E\subseteq\mathcal{A}^2$, say that $E$ is $\mathfrak{L}$-equality-like iff:

*

*$E$ is an equivalence relation.


*$E$ satisfies the substitution scheme for $\mathfrak{L}$-formulas: if $(a_i)_{i<\theta},(b_i)_{i<\theta}$ are (possibly infinite!) tuples of elements of $\mathcal{A}$ with $a_iEb_i$ for each $i$ and $\varphi$ is a $\theta$-ary $\mathfrak{L}$-formula with parameters from $\mathcal{A}$, then $$\mathcal{A}\models\varphi((a_i)_{i<\theta})\quad\iff\quad\mathcal{A}\models\varphi((b_i)_{i<\theta}).$$
Now if $\mathcal{A}$ is a structure and $E$ is a congruence on $\mathcal{A}$, the quotient structure $\mathcal{A}/E$ is well-defined. Every $\mathfrak{L}$-equality-like relation is a congruence a fortiori, so we can ask how similar $\mathcal{A}$ and $\mathcal{A}/E$ are guaranteed to be assuming $E$ is $\mathfrak{L}$-equality-like. If "equivalence relation + substitution scheme" truly captures the nature of equality as far as $\mathfrak{L}$ is concerned, the answer should be "as similar as possible:"

Say that $\mathfrak{L}$ is simple for equality iff $\mathcal{A}\equiv_\mathfrak{L}\mathcal{A}/E$ whenever $\mathcal{A}$ is a structure and $E$ is an $\mathfrak{L}$-equality-like relation on $\mathcal{A}$.

Trivially, any logic with equality built in directly (such as full first-order logic) is simple-for-equality, since in such a logic the only equality-like relation is equality itself so we always have $\mathcal{A}\cong\mathcal{A}/E$ if $E$ is equality-like. Less trivially, the point of the previous section of this answer was exactly that $\mathsf{FOL_{w/o=}}$ is also simple-for-equality.
However, not every logic is simple-for-equality. For example, consider the logic gotten by adding the quantifier "There is exactly one" to first-order logic without equality. The result $\mathfrak{L}_{\mathsf{weird}}$ is a logic intermediate between first-order logic without equality and full first-order logic (note that in full first-order logic we can express "There is exactly one $x$ such that $\varphi$" as "$\exists x\forall y[\varphi(x)\wedge(\varphi(y)\leftrightarrow x=y)]$"). It's easy to see that $\mathfrak{L}_{\mathsf{weird}}$ is not simple-for-equality: consider a pure set $\mathcal{A}$ with two elements and the sentence "There is exactly one $x$ such that $\top$." Since full first-order logic is trivially simple for equality, this shows that we can have a non-simple-for-equality logic lying "between" two logics which are each simple-for-equality, so the situation is a bit complicated.
Now intuitively $\mathfrak{L}_{\mathsf{weird}}$, as the name indicates, is a bit silly. In a sense it's trying to have its cake and eat it too: on the one hand we remove equality from our logic in order to have lots of equality-like relations, but on the other hand the "There is exactly one" quantifier implicitly refers to equality on its own. This raises the hope that all "natural" logics are simple-for-equality, and certainly all the examples I can think of are. Unfortunately, at the moment I don't know of a satisfying, non-ad-hoc criterion guaranteeing simplicity-for-equality, so I'm not entirely confident about this.
