Is “forall elimination twice with the same fresh variable” allowed?

I am looking to prove that $\forall x \forall y \; P(x,y) \vdash \forall x \; P(x,x)$ and I wonder if this is allowed: 1. ∀x ∀y P(x,y) Premise 2. | x0 fresh variable 3. | ∀y P(x0, y) ∀-elimination (1) 4. | P(x0, x0) ∀-elimination (3) 5. ∀x P(x, x) ∀-introduction (4) 

It's the second forall elimination that I am worried about being incorrect. If this is not allowed, I would like to know why that is the case.

• It's fine.${{}}$ – Git Gud Sep 22 '16 at 13:34
• @GitGud, do you happen to have a source of sort that points towards this? I am reading the book "Logic in Computer Science" by Huth and Ryan, but I cannot find anything that supports this. – GLaDER Sep 22 '16 at 13:40
• The rules themselves support it. Sorry, I don't know about any source that singles out this issue specifically. – Git Gud Sep 22 '16 at 13:44
• See page 109: "The rule] says: If $∀xφ$ is true, then you could replace the $x$ in $φ$ by any [emphasis added] term $t$ (given, as usual, the side condition that $t$ be free for $x$ in $φ$) and conclude that $φ[t/x]$ is true as well." When we have "nested" universal quantifiers, the condition still apply : any term $t$. The intuition is : "for all" means ... for all. – Mauro ALLEGRANZA Sep 22 '16 at 13:52

For the second forall elimination any name may be used to stand for the variable $$y$$ including the name used for the first forall elimination of variable $$x$$.