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.