axioms of equality

The second formula is an axiom of the first order logic with equality, together with the following axioms about equality:

1. $x=x$.
2. $x=y\rightarrow(\varphi\leftrightarrow\psi)$, where and $y$ is free for $x$ in $\varphi$ and $\psi$ is replacing some free variable $x$ by $y$ in $\varphi$.

Unlike Extensionality, which is a proper axiom, these equality axioms are valid in every normal models, hence they deserve the name "logical axioms".

The second fact is a special case of the indiscernibility of identicals and is part of the definition of equality. The principle says, for all predicates $\phi (u, t_1, t_2, \ldots, t_n)$, $$\forall x . \forall y . (x = y) \to (\phi (x, t_1, t_2, \ldots, t_n) \leftrightarrow \phi (y, t_1, t_2, \ldots, t_n))$$ where $t_1, t_2, \ldots, t_n$ are arbitrary parameters. For the language of set theory in first-order logic without equality, the special case implies the general principle.