\begin{definition}[Definition:Freely Substitutable]
Let $\mathbf C$ be a WFF of predicate logic.
Let $x$ be a variable in $\mathbf C$.
Let $\phi \left({y_1, \ldots, y_n}\right)$ be a term in which the variables $y_1, \ldots y_n$ occur.
Then $\phi \left({y_1, \ldots, y_n}\right)$ is '''freely substitutable for $x$ in $\mathbf C$''' {{iff}} no free occurrence of $x$ occurs in a well-formed part of $\mathbf C$ which is of the form:
:$( Q y_i: \mathbf B )$
where $Q$ is a quantifier and $\mathbf B$ is a WFF.
\end{definition}