List of axioms:
$(A1)$ - All Tautologies.
$(A2)$ - $(\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)) $.
$(A3)$ - $(\forall x \alpha) \rightarrow [\alpha]^{t}_{x} $ if x is free for t in $\alpha$.
$(A4)$ - $\alpha \rightarrow (\forall x \alpha) $ if x is not free in $\alpha $.
$(A5)$ - $ x = x$
$(A6)$ - $(x=y) \rightarrow (\alpha \rightarrow \beta)$ if $\beta$ if obtained by substitution of at least one occurrence of x free for y in $\alpha$.
Modus Ponens as inference rule.
Generalization Theorem:
If $\Gamma \vdash \phi$ and x do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \phi$
And Deduction Theorem.
Again, the strategy is to prove: $\vdash P(y) \rightarrow \forall x(x=y \rightarrow P(x))$
and the converse.
I tried to use (A6) and got stuck with $(x=y) \rightarrow (P(y) \rightarrow P(x))$ after proving that $(x=y) \rightarrow (y=x)$
For the converse, I reach $(x=y) \rightarrow P(x)$ and need to prove $P(y)$. How do I suppose to prove $P(y)$ in this condition?
Is there an easier way to prove this theorem?