Ηere: Equality and its axioms, the rule of substitution of functions is placed among the axioms of equality, but at the same time, it says "is (equivalent to) a special case of the third schema", that is, the axiom schema of substitution of formulas. Then, why is it an axiom? Further more, many writers use it as an axiom, along with substitution of formulas.
It is easy to prove it, I think: Let $f:D\mapsto C$ be any function and $x,y\in D $.
$x=y $ (premise)
$f(x)=f(x) $ (axiom of reflexivity)
$x=y\rightarrow\left[f(x)=f(x)\rightarrow f(x)=f(y)\right] $ (axiom of substitution of formulas)
$f(x)=f(x)\rightarrow f(x)=f(y) $ (MP 3,1)
$f(x)=f(y) $ (MP 4,2)
$x=y\vdash f(x)=f(y) $, thus: $x=y\rightarrow f(x)=f(y) $ and with un. generalization, $\forall x\forall y\left(x=y\rightarrow f(x)=f(y)\right) $.
$f$ could be any function, and although we can not state this in a FOL lanquage, we have proved a schema of a theorem.
So, why it is so often placed as an axiom? Is there any reason for that?