\begin{definition}[Definition:Semantic Equivalence/Predicate Logic/Definition 1]
Let $\mathbf A, \mathbf B$ be WFFs of predicate logic.
Then $\mathbf A$ and $\mathbf B$ are '''equivalent''' {{iff}}:
:$\mathbf A \models_{\mathrm{PL_A}} \mathbf B$ and $\mathbf B \models_{\mathrm{PL_A}} \mathbf A$
that is, each is a semantic consequence of the other.
That is to say, $\mathbf A$ and $\mathbf B$ are '''equivalent''' {{iff}}, for all structures $\AA$ and assignments $\sigma$:
:$\AA, \sigma \models_{\mathrm{PL_A}} \mathbf A$ {{iff}} $\AA, \sigma \models_{\mathrm{PL_A}} \mathbf B$
where $\models_{\mathrm{PL_A}}$ denotes the models relation.
\end{definition}