Isn’t $P\rightarrow\forall xP$ the Generalisation Theorem?

Question

The logical axioms I’m concerned with are mentioned in Wolf’s A Tour Through Mathematical Logic, Appendix A A Deductive System for First-order Logic which Wolf claims to have taken from Enderton’s book. These are:

Logical axioms

The logical axioms are all generalisations of all formulas of the following types.

1. All tautologies.
2. Universal specification: $\forall xP(x)\rightarrow P(t)$, where $t$ is a term of the same sort as the variable $x$, $P(t)$ is the result of replacing all free occurrences of $x$ in $P(x)$ by $t$, and no free variable of $t$ becomes bound in $P(t)$.
3. $\forall x(P\rightarrow Q)\rightarrow (\forall xP\rightarrow\forall xQ)$.
4. $P\rightarrow\forall xP$, where $x$ does not occur free in $P$.
5. Definition of $\exists$: $\exists P\leftrightarrow\neg\forall x\neg P$.
6. $x=x$.
7. Substitution of equals: $x=y\rightarrow [P(x)\leftrightarrow P(y)]$, where $P$ is atomic and $P(y)$ is the result of replacing one or more occurrences of $x$ in $P(x)$ by $y$.

Rule of inference

1. Modus ponens: From two steps of the form $P$ and $P\rightarrow Q$, $Q$ may be concluded.

Question: Isn’t the fourth logical axiom the Generalisation Theorem?