Considering that the logic axioms of first order logic are given by:
$(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$.
Are the following formulas logic axioms, following this definition? For the formulas that are logic axioms, in which group of axioms is the formula based?
I - $x = y \rightarrow (y=z \rightarrow z=x)$
II - $\forall w \exists x (P(w,x)\rightarrow P(w,w)) \rightarrow \exists x (P(x,x)\rightarrow P(x,x)))$
III - $\forall x(\forall x(c = f(x,c) \rightarrow \forall x\forall x(c= f(x,c))))$
IV - $\forall x((0<x) \rightarrow (0<x+x)) \rightarrow ((0<x) \rightarrow \forall x(0<x+x))$
For example, I is something like (A6), but I can't see if $\beta$ in this case is obtained of $\alpha$ by substitution of at least one occurrence of x free for y.
Considering II, I know it is something like (A3), but when we substitute w for x, because of the $\exists x$, is it a logic axiom?
Considering III, we have something like $\forall x(\forall x \alpha \rightarrow \forall x(\forall x\alpha))$, where $\alpha$ is $c=f(x,c)$. How do I proceed with the analysis? Same case for the generalization of $(0<x+x)$ in IV.