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.