Is there a complete set of equivalence principles for first-order logic?

Question

There is a sound and complete set of equivalence principles for classical propositional logic in the sense that for all propositional logic sentences $\varphi$ and $\psi$: $\varphi$ and $\psi$ are logically equivalent if and only if through the application of these equivalence principles, $\varphi$ and be transformed into $\psi$.

Here is such a set:

Double Negation

$\neg \neg P \Leftrightarrow P$

Commutation

$P \land Q \Leftrightarrow Q \land P$

$P \lor Q \Leftrightarrow Q \lor P$

Association

$P \land (Q \land R) \Leftrightarrow (P \land Q) \land R$

$P \lor (Q \lor R) \Leftrightarrow (P \lor Q) \lor R$

DeMorgan

$\neg(P \land Q) \Leftrightarrow \neg P \lor \neg Q$

$\neg(P \lor Q) \Leftrightarrow \neg P \land \neg Q$

Distribution

$P \land (Q \lor R) \Leftrightarrow (P \land Q) \lor (P \land R)$

$P \lor (Q \land R) \Leftrightarrow (P \lor Q) \land (P \lor R)$

Idempotence

$P \land P \Leftrightarrow P$

$P \lor P \Leftrightarrow P$

Complement

$P \land \neg P \Leftrightarrow \bot$

$P \lor \neg P \Leftrightarrow \top$

Identity

$P \land \top \Leftrightarrow P$

$P \lor \bot \Leftrightarrow P$

To prove that this set is complete, you can show that this set of equivalences allows you to put any propositional logic statement into its 'canonical CNF (or DNF)'

My question is: is there such a (finite!) set for first-order logic?

My thoughts:

First, let's list some basic FOL equivalences:

Quantifier Negation

Where $\varphi$ is any formula and $x$ and any variable:

$\neg \exists x \ \varphi \Leftrightarrow \forall x \ \neg \varphi$

$\neg \forall x \ \varphi \Leftrightarrow \exists x \ \neg \varphi$

Null Quantification

Where $\varphi$ is any formula that does not have $x$ as a free variable:

$\forall x \ \varphi \Leftrightarrow \varphi$

$\exists x \ \varphi \Leftrightarrow \varphi$

Replacing Variables

With $x$ and $y$ any variables, and where the free variables $x$ in $\varphi(x)$ occur on the same place as the free variables $y$ in $\varphi(y)$, and where $\varphi(x)$ and $\varphi(y)$ are otherwise the same:

$\forall x \ \varphi(x) \Leftrightarrow \forall y \ \varphi(y)$

$\exists x \ \varphi(x) \Leftrightarrow \exists y \ \varphi(y)$

Swapping Quantifiers of Same Type

$\forall x \forall y \ \varphi(x,y) \Leftrightarrow \forall y \forall x \ \varphi(x,y)$

$\exists x \exists y \ \varphi(x,y) \Leftrightarrow \exists y \exists x \ \varphi(x,y)$

Quantifier Distribution

$\forall x (\varphi(x) \land \psi(x)) \Leftrightarrow \forall x \ \varphi(x) \land \forall x \ \psi(x)$

$\exists x (\varphi(x) \lor \psi(x)) \Leftrightarrow \exists x \ \varphi(x) \lor \exists x \ \psi(x)$

Prenex Laws

Where $\varphi$ is any formula and where $x$ is not a free variable in $\psi$:

$ \forall x \ \varphi \land \psi \Leftrightarrow \forall x (\varphi \land \psi)$

$ \psi \land \forall x \ \varphi \Leftrightarrow \forall x (\psi \land \varphi)$

$ \exists x \ \varphi \land \psi \Leftrightarrow \exists x (\varphi \land \psi)$

$ \psi \land \exists x \ \varphi \Leftrightarrow \exists x (\psi \land \varphi)$

$ \forall x \ \varphi \lor \psi \Leftrightarrow \forall x (\varphi \lor \psi)$

$ \psi \lor \forall x \ \varphi \Leftrightarrow \forall x (\psi \lor \varphi)$

$ \exists x \ \varphi \lor \psi \Leftrightarrow \exists x (\varphi \lor \psi)$

$ \psi \lor \exists x \ \varphi \Leftrightarrow \exists x (\psi \lor \varphi)$

Now, using the Prenex Laws, together with Quantifier Negation and Swapping Variables, and all the propositional logic equivalences listed earlier all FOL statements can be put into Prenex Normal Form (is that right?) ... so I was thinking that maybe one could show that all FOL statements can be put into some kind of 'canonical PNF' (and here something like Swapping Quantifiers of Same Type would probably come in handy) ... but what would that look like?

On the other hand, the Distribution of $\forall$ over $\land$, and $\exists$ over $\lor$ feel 'nasty' to me ... I assume I cannot prove them from the others ... which makes me feel that there are probably lots of such other 'nasty interplays' that would require such a principle ... and probably non-recursively many.

Then again, completeness of FOL gives me hope that there is a complete set ... but then the undecidability of FOL makes me fear there is not such a set. I can't really wrap my head around as to which result would be more applicable here.