Unifier

If we let $S$ be a substitution and $\varphi$ and $\phi$ be two first order formulas: Then $S$ unifies, or is a unifier for, $\varphi$ and $\phi$ if $S(\varphi )=S(\phi )$.