\begin{definition}[Definition:Alphabetic Substitution]
Let $\mathbf C$ be a WFF of the language of predicate logic $\LL_1$.
Consider the (abbreviated) WFF $Q x: \mathbf C$.
Let $y$ be another variable such that $y$ does not occur in $\mathbf C$.
Let $\mathbf C'$ be the WFF resulting from replacing all free occurrences of $x$ in $\mathbf C$ with $y$.
Then to all intents and purposes, the WFFs:
:$Q x: \mathbf C$
:$Q y: \mathbf C'$
will have the same interpretation.
Thus we may change the free occurrences of any variable for another variable symbol.
This change is called '''alphabetic substitution'''.
\end{definition}