This is the answer to the final question.

Where is that “Let …” sentence coming from? I never see this syntax in a formal proof in the book or the lecture. (I haven’t read all the parts of the solution though)

I suppose I should write a formal proof and it should be proving

(All the comma here should be a dot)

While instead, the answer has two free variables here. The reason I think the proof in the solution cannot be used to prove the sentence above with quantifier is that as far as I know we have never been introduced some rules like below:

The only way to introduce the universal quantifier is at the back of the book.