Formula equivalence (first-order logic)
From Learning Logic for Computer Science
First-order formulas are equivalent if they evaluate to the same truth value in every structure under every variable assignment.
Equivalence of objects is always defined in the same way and to the same effect: objects are considered equivalent when they behave the same in all possible contexts (or contexts considered interesting); equivalent objects can be replaced for one another in all possible contexts (or contexts considered interesting).
For first-order formulas, this is spelled out in what follows.
Definition First-order formulas $\varphi$ and $\psi$ over a signature $\mathcal S$ are equivalent, $\varphi \SemEquiv \psi$ in symbols, if $$[\![\varphi]\!]_\beta^\mathcal A = [\![\psi]\!]_\beta^\mathcal A$$ holds for every $\mathcal S$-structure $\mathcal A$ and $A$-variable assignment $\beta$.
The relation $\SemEquiv$, defined between first-order formulas, satisfies all properties known from equivalence relations.
The proof is straightforward.
Congruence property and further properties of the equivalence relation
An important property is that the equivalence relation is compatible with every connective and with both quantifiers.
A more general variant of this lemma states that if in a given first-order formula a subformula is replaced by an equivalent formula, then the resulting formula is equivalent to the given one.
The list of basic equivalences between propositional formulas hold for first-order logic.
There are additional laws for quantifiers.