some valid schemas of first order logic

In this entry, we record some valid schemas of first order logic FO$(\mathrm{\Sigma })$ based on the signature $\mathrm{\Sigma }$:

1. $\forall xA\to \forall yA[y/x]$ if $y$ does not occur free, but free for $x$, in $A$

2. $\forall yA[y/x]\to \forall xA$ if $y$ does not occur in $A$

3. $\forall xA\leftrightarrow A$ if $x$ is not free in $A$

4. $\exists xA\leftrightarrow A$ if $x$ is not free in $A$

5. $\forall x\forall yA\to \forall y\forall xA$

6. $\exists x\exists yA\to \exists y\exists xA$

7. $\forall x(A\to B)\to (\forall xA\to \forall xB)$

8. $(\forall xA\to \forall xB)\to \forall x(A\to B)$

9. $\forall x(A\wedge B)\leftrightarrow \forall xA\wedge \forall xB$

10. $\exists x(A\vee B)\leftrightarrow \exists xA\vee \exists xB$

11. $\forall x(A\vee B)\leftrightarrow (\forall xA)\vee B$ if $x$ is not free in $B$

12. $\exists x(A\wedge B)\leftrightarrow (\exists xA)\wedge B$ if $x$ is not free in $B$

where $A,B$ are well-formed formulas (wff’s) of FO$(\mathrm{\Sigma })$.