Deriving symmetry of equality in FOL

Question

In FOL with equality, the axioms of equality are:

1. $\forall x(x=x).$
2. Let $\varphi$ be a formula with free occurences of $x$, and define $\varphi'$ by replacing some or all of the free occurences of $x$ in $\varphi$ with $y$, then $\forall x\forall y(x=y\rightarrow(\varphi\rightarrow\varphi')).$

The symmetric property of equality becomes a theorem that follows from these, and I've tried the following:

Let $\varphi\equiv x=x$ and $\varphi'\equiv y=x$, then by the second schema: $$\forall x\forall y(x=y\rightarrow(x=x\rightarrow y=x)).$$ It's pretty tempting to proceed as follows: $$\forall x\forall y(x=y\rightarrow(\top\rightarrow y=x))$$ $$\forall x\forall y(x=y\rightarrow y=x).$$ My doubt however is, is it wrong to assume that the formula $x=x$ is always true, even when all occurences of $x$ are unbound? Does the universal quantification shown in the first axiom make a difference?

Answer 1

is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?

No, it works.

More detailed proof :

1) $\vdash \forall x (x=x)$ --- axiom 1

2) $\vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (\phi[z/x] → \phi[z/y]))$, where $\phi(z) := (z=x)$

3) $x=y$ --- assumed [a]

4) $x=x$ --- from 1) by $\forall$-elim (i.e. Universal Instantiation)

5) $x=y → (x=x → y=x)$ --- from 2) by $\forall$-elim

6) $(x=x → y=x)$ --- from 3) and 5) by $\to$-elim (aka Modus Ponens)

7) $y=x$ --- from 4) and 6)

8) $(x=y \to y=x)$ --- from 3) and 7) by $\to$-intro (aka Conditional Proof), discharging [a]

$\vdash ∀x∀y(x=y \to y=x)$ --- from 8) by $\forall$-intro (i.e. Universal generalization) twice.