I'm trying to simplify some of my notes on FOL, and I came across a proposition that would greatly help me make much fewer messes.
Let $T$ be a theory in FOL, and suppose $T \vdash \exists_y p(x, y)$.
(If necessary, add also the constraint $T \vdash p(x,y) \wedge p(x, y') \rightarrow y = y'$)
Let $T'$ be the same theory, with a new function symbol $f$ added, with the axiom $p(x, f(x))$.
I wish to show that anything I can prove in $T'$ I can prove in $T$. That is, given a formula $\phi$ of $T$, if $T' \vdash \phi$ then $T \vdash \phi$.
I have managed to show an analogous proposition regarding the addition of propositional symbols, but the version of adding function symbols is proving more troublesome than I expected.
The book where I found this proposition (Schoenfield) uses some tools I'm trying to avoid unless I really have to use them, such as Prenex form and Herbrand's theorem. This seems like it should be doable in a more or less elementary way, but after butting my head against the wall for a few days I have come to math.stackexchange for help.