Suppose $x$ and $y$ are distinct variables, and $r,s,t$ are terms. We do induction on the complexity of $t$.

1. 1.

   First, suppose $t$ is a constant symbol. Then LHS and RHS are both $t$.

2. 2.

   Next, suppose $t$ is a variable.

   • If $t$ is $x$, then LHS $=s[r/y]$, and since $y$ is not $x$, RHS $=x[s[r/y]/x]=s[r/y]$.

   • If $t$ is $y$, then LHS $=y[r/y]=r$, since $x$ is not $y$, and RHS $=r[s[r/y]/x]=r$, since $x$ does not occur in $r$.

   • If $t$ is neither $x$ nor $y$, then both sides are $t$.

   In all three cases, LHS $=$ RHS.

3. 3.

   Finally, suppose $t$ is of the form $f(t_{1},\ldots,t_{n})$. Then LHS $=f(t_{1}[s/x],\ldots,t_{n}[s/x])[r/y]=f(t_{1}[s/x][r/y],\ldots,t_{n}[s/x][r/y])$, which, by induction, is

   $$f(t_{1}[r/y][s[r/y]/x],\ldots,t_{n}[r/y][s[r/y]/x])$$

   or $f(t_{1}[r/y],\ldots,t_{n}[r/y])[s[r/y]/x]=f(t_{1},\ldots,t_{n})[r/y][s[r/y]/x]=$RHS.

∎

Suppose $x$ and $y$ are distinct variables, $s,t$ terms, and $A$ a wff. We do induction on the complexity of $A$.

1. 1.

   First, suppose $A$ is atomic.

   • $A$ is of the form $t_{1}=t_{2}$, then LHS is $t_{1}[t/x][s/y]=t_{2}[t/x][s/y]$ and we can apply the previous equation to both $t_{1}$ and $t_{2}$ to get RHS.

   • If $A$ is of the form $R(t_{1},\ldots,t_{n})$, then LHS is $R(t_{1}[t/x][s/y],\ldots,t_{n}[t/x][s/y])$, and we again apply the previous equation to each $t_{i}$ to get RHS.

2. 2.

   Next, suppose $A$ is of the form $B\to C$. Then LHS $=B[t/x][s/y]\to C[t/x][s/y]$, and, by induction, is $B[s/y][t[s/y]/x]\to C[s/y][t[s/y]/x]=$ RHS.

3. 3.

   Finally, suppose $A$ is of the form $\exists zB$.

   • $x$ is $z$. Then $A[t/x][s/y]=A[s/y]$, and $A[s/y][t[s/y]/x]=A[s/y]$ since $x$ is bound in $A[s/y]$.

   • $x$ is not $z$. Then $A[t/x][s/y]=(\exists zB[t/x])[s/y]$.

     • $y$ is $z$. Then $(\exists zB[t/x])[s/y]=\exists zB[t/x]$. On the other hand, $A[s/y][t[s/y]/x]=A[t[s/y]/x]=\exists zB[t[s/y]/x]$. By induction, $t,s$ are free for $x,y$ in $B$, and $B[t/x]=B[t[s/y]/x]$, the result follows.

     • $y$ is not $z$. Then $(\exists zB[t/x])[s/y]=\exists zB[t/x][s/y]$. On the other hand, $A[s/y][t[s/y]/x]=(\exists zB[s/y])[t[s/y]/x]=\exists zB[s/y][t[s/y]/x]$ since $x$ is not $z$. By induction again, $t,s$ are free for $x,y$ in $B$, and $B[t/x]=B[t[s/y]/x]$, the result follows once more.

∎