Precise axiomatic definition for the equality "=" as a binary relation

Question

Question: What is a simple yet precise definition for "=" as a binary relation?

My try: I find two definitions for "equality relation" which seems to be contradictory.

The first one I learnt in school is that equality is what is called an equivalence relation, that is, it satisfies three axioms: Reflexivity, Symmetry, Transitivity.

The second definition contains an axiom of extensionality.

The third definition I heard contains this additional axiom: $x=y$ implies $P(x)=P(y)$

---

Thanks to the comments, I also learnt a definition using first-order logics:

These equality axioms are:

1. Reflexivity.
2. Substitution for functions.
3. Substitution for formulas.

This is close to the things I am looking for. However, this definition looks weird as the second axiom is a special case of the third. Axiomatic system usually don't use redundant axioms.

Answer 1

Re your addendum to the question.

Yes, the two basic axioms for equality are reflexivity: $x=x$, and substitution for formulas: $s = t \to (\varphi [s/z] \to \varphi [t/z])$.

Note that, using Universal instantiation, we have that reflexivity holds for terms whatever: $t=t$.

Now, if $f$ is a function symbol (assuming for simplicity that it is a unary function symbol) from reflexivity we have $f(x)=f(x)$.

Thus, having that $f(x)=f(x)$ is $(z=f(x))[f(x)/z]$ and $f(y)=f(x)$ is $(z=f(x))[f(y)/z]$ we can use susbstitution to get:

$x=y \to f(x)=f(y)$.

The substitution property is crucial for equality: if the binary relation has reflexivity, symmetry and transitivity but lacks the substitution property its is an equivalence relation.