 Solution

Fix any structure and any assignment of the three quantified variables, writing their values as $a_0,a_1,a_2$. If either of the nested antecedents is false, the corresponding implication is true. If both are true, then $f^A(a_0)=a_1$ and $f^A(a_0)=a_2$. Actual identity is transitive, so $a_1=a_2$, making the consequent true as well.

Thus the unquantified matrix is true under every assignment in every structure. The universal-quantifier semantic clause then makes its universal closure true in every structure:No assumption that $f$ is injective is used. The argument says that one value cannot equal two distinct elements, not that distinct inputs have distinct outputs.