The techique is in Bell & Machover: A course in mathematical logic, ch 2 §10 as theorem 10.5.

It states…

Select an $n$-ary function symbol $\mathbf f$ of $\mathcal L$, and let $\mathcal L'$ be obtained from $\mathcal L$ by excluding $\mathbf f$ and introducing a new $(n+1)$-ary predicate symbol $P$. We prove:

Theorem. For any $\mathcal L$-formula $\mathbf \alpha$ we can find an $\mathcal L'$-formula which is co-satisfiable with $\mathbf \alpha$ and an $\mathcal L'$ formula which is co-valid with $\mathbf \alpha$.

[Google books link.][1]


  [1]: https://books.google.se/books?id=937NCgAAQBAJ&pg=PA100&lpg=PA100&dq=eliminating%20function%20symbols%20first%20order%20logic&source=bl&ots=TKc1pGK_fQ&sig=8poasl8aOt2fSAq15MpMAnyQI_Y&hl=en&sa=X&redir_esc=y#v=onepage&q=eliminating%20function%20symbols%20first%20order%20logic&f=false