Showing that $\neg[ Px\rightarrow \forall xPx]\vdash \forall xPx$ via generalization theorem Let $P$ be a unary relation, we want to show that: 
If $\neg[ Px\rightarrow \forall xPx]\vdash Px$ then $\neg[ Px\rightarrow \forall xPx]\vdash \forall xPx$.
I want to do that via generalization theorem  but $x$ is free in $\neg[ Px\rightarrow \forall xPx]$ so I can't use the theorem here. I've to change the free $x$ to another variable say $y$, So, now we have 
$$\neg[ Px\rightarrow \forall xPx]\vdash Py$$ and we then can use generalization theorem to obtain $\neg[ Px\rightarrow \forall xPx]\vdash \forall y Py$ which is $$\neg[ Px\rightarrow \forall xPx]\vdash \forall x Px$$ and we are done. In changing $x$ into $y$, we have assumed implicitly that $Px\vdash Py$
My question is: How to show that $Px\vdash Py$? How to justify this changing of variables from $x$ into $y$?

You haven't said exactly what logic you are working in, but the deduction you are trying to make is not correct in the usual formulations of first order logic. To see this, note that $\lnot(A \rightarrow B)$ is equivalent to $A \land \lnot B$. If you interpret $Px$ as $x = 1$ in the theory of the natural numbers, then $\lnot[Px \rightarrow \forall xPx] \vdash Px$ (i.e., $x = 1 \land \exists x (\lnot x = 1) \vdash x = 1$) is true, but  $\lnot[Px \rightarrow \forall xPx] \vdash \forall xPx$ (i.e. $x = 1 \land \exists x (\lnot x = 1) \vdash \forall x(x = 1)$) is not. Are you sure you have written the quantifiers down correctly?
