Let $\phi$ be a first-order formula, and let $\phi_t^x$ be the formula $\phi$ with term $t$ substituted for variable $x$.
Exercise 6 in section 1.8 of Leary and Kristiansen’s A Friendly Introduction to Mathematical Logic asks when $(\phi_y^x)_x^y$ is $\phi$. The solution says: if and only if $y$ is substitutable for $x$ in $\phi$.
Is this not wrong? If $\phi$ is $\forall x(x=y)$, then $y$ is substitutable for $x$ in $\phi$, but $(\phi_y^x)_x^y$ is $\forall x (x = x)$. Shouldn’t the condition include that $x$ be substitutable for $y$ in $\phi$ as well?
The problem is not connected to quantification: $Py$ is a counterexample as well since $((Py)^x_y)^y_x = Px$. The solution should be: $y$ not part of $\phi$; therefore $((\phi)^x_y)^y_x = \phi$. Proof: Induction on terms then on formulas.