Not understanding the solution of exercise 2.39 in Mendelson.

Question

This question is from "Introduction to Mathematical Logic" by Elliot Mendelson , fourth edition.

At page $83$ , I was given the following theorem to prove at exercise $2.39$:

$\vdash \lnot (\exists y)(\forall x)(A^2_1(x,y) \leftrightarrow \lnot A^2_1(x,x))$

After some tries I gave up proving , so I looked up the solutions in the book . Here is the solution of the book (page 390):

1. $\vdash (\exists y)(\forall x)(A^2_1(x,y) \leftrightarrow \lnot A^2_1(x,x))$ [Hype]
2. $(\forall x)(A^2_1(x,b) \leftrightarrow \lnot A^2_1(x,x))$ [1,rule C]
3. $(A^2_1(b,y) \leftrightarrow \lnot A^2_1(b,b))$ [2, rule A4]
4. $\mathscr C \land \lnot \mathscr C$ [3 , tautology]

($\mathscr C$ is any wf not containing $b$.) Use Proposition $2.10$ and proof by contradiction.$\square$

But there are soe places I didn't understand at all.

1. When applying rule A4 to line 2 , shouldn't it be $(A^2_1(b,b) \leftrightarrow \lnot A^2_1(b,b))$ instead of $(A^2_1(b,y) \leftrightarrow \lnot A^2_1(b,b))$
2. I have no idea how the book derived line 4 from line 3.