The Interpretation Theorem is the following excerpt from Kunens old Set Theory
8. Appendix $1$: More on relativization
We sketch here a more formal treatment than that in $\S 2$. There is a general notion of relativization in logic, but we shall discuss only the special case of interest for set theory.
A relative interpretation of set theory into itself consists of two formulas, $\mathbf{M}(x,v)$ and $\mathbf{E}(x,y,v)$, with no free variables other than the ones shown. We think of $v$ as a parameter defining the class $\{ x: \mathbf{M}(x,v) \}$ with binary relation $\{ \langle x, y \rangle : \mathbf{E}(x,y,v) \}$. If $\phi$ is a formula, we define $\phi^{\mathbf{M}, \mathbf{E}}$ by replacing $x \in y$ by $\mathbf{E}(x,y,v)$ and restricting the bound variables to range over $\mathbf{M}$. In $\S\S 1-7$, $\mathbf{E}(x,y,v)$ was always $x \in y$. In the case of $\mathbf{WF}$, where we discuss a fixed model, the parameter $v$ does not appear in $\mathbf{M}$. However, when discussing set models, $\mathbf{M}(x,v)$ is formally $x \in v$, so that results in $\S 7$ of the form $\exists M( \phi^M)$ would be written $\exists v (\phi^{x \in v, x \in y})$ in our present notation.
To see that relativization yields relative consistency proofs, one must first check the following.
$8.1.$ LEMMA. If $\phi_1, \ldots, \phi_n, \psi$ are sentences , $\phi_1, \ldots, \phi_n \vdash \psi$, and $\mathbf{M}$, $\mathbf{E}$ are as above, then
$$ \vdash \forall v \Big [ \big [ \exists x \mathbf{M}(x,v) \land \phi_1^{\mathbf{M}, \mathbf{E}} \land \cdots \land \phi_n^{\mathbf{M}, \mathbf{E}} \big ] \to \psi^{\mathbf{M}, \mathbf{E}} \Big].$$
PROOF. Similar to the easy direction of the Gödel Completeness Theorem. $\square$
The name is from Shoenfields Mathematical Logic. Shoenfield proves essentially the same theorem for a very small Hilbert-style proof-stystem that is very far removed from being able to transcribe even the simplest proofs to a formal one, so I tried to actually prove the Theorem for a natural deduction system. Lets use standard $x\in y$ for $E(x,y,v)$.
Essentially we have to check, that each deduction step also works for the relativized version of the Formula. The only hard cases involve of course Quantifiers. We can do away with e.g. the existential quantifiers by defining them by $\neg\forall\neg$. So this is where i am stuck:
The $\forall$-Elimination requires me to show that if in the original proof we have inferred $A(r)$ from $\forall x: A(x)$ that we can in the relativized proof infer $A(r)^M$ (which is $A^M(r)$) from $[\forall x: A(x)]^M$ (which is $\forall x (M(x)\rightarrow A^M(x))$).
By Application of $\forall$-E we only get $M(r)\rightarrow A^M(r)$ so we are left to argue that $r$ can be made to be from $M$. What is the magic needed here?
I tried to study the proof that you can infer $\exists x:A(x)$ from $\forall x:A(x)$ and relativized the proof. We need the $\exists x: M(x)$ there. But i dont see how to put that into the above proof.
I'm going to give you the model-theoretic proof, despite the fact that you said in the comments that it's not what you're looking for, just so you can see how obvious the statement is when you look at it from a semantic point of view.
And I can't help making a meta-comment: of course there are good reasons to try to prove things in weak meta-theories. But in my opinion, it's only worth worrying about what meta-theoretic principles are necessary to develop a body of mathematics after you already understand that body of mathematics. I would strongly recommend when first learning logic to allow yourself to use all the tools of ordinary mathematics when proving things. That way you can more easily develop intuition and clearly see which things are easy and which are more significant results.
First, let's be clear about what the completness theorem says. For any first-order theory $T$ and any sentence $\varphi$, $T\models \varphi$ if and only if $T\vdash \varphi$. One direction of this bi-implication is soundness: If $T$ proves $\varphi$, then every model of $T$ satisfies $\varphi$. The other direction is completeness: If every model of $T$ satisfies $\varphi$, then $T$ proves $\varphi$. But the point is that $\vdash$ and $\models$ are interchangeable in the context of first-order logic.
In the comments, you expressed some skepticism that we can use a model-theoretic argument for the lemma, because of the distinction between set models (those whose domains are sets) and proper class models. Let me emphasize that in the statement of the completeness theorem and in the proof below, all $L$-structures are sets. The definition of $\models$ only quantifies over set models, so to give model-theoretic proofs about $\vdash$ using the completeness theorem, we only need to consider set models.
Next, we turn to relativization. Fix $L$ to be the language of set theory, and fix $L$-formulas $M(x,v)$ and $E(x,y,v)$. For any $L$-structure $(U,\varepsilon)$ and any $c\in U$, we define $M_c = \{a\in U\mid U\models M(a,c)\}$ and $E_c = \{(a,b)\in M_c\mid U\models E(a,b,c)\}$. Then (as long as $M_c$ is non-empty) we have a non-empty set $M_c$ and a binary relation $E_c$ on $M_c$, so $(M_c,E_c)$ is a new L-structure.
One can easily prove by induction and that for any formula $\varphi$, $M_c\models \varphi$ if and only if $U\models \varphi^{M,E}(c)$.
Finally let's prove Lemma 8.1. Let $\varphi_1,\dots,\varphi_n,\psi$ be sentences such that $\varphi_1,\dots,\varphi_n\vdash \psi$. Then $\varphi_1,\dots,\varphi_n\models \psi$ by soundness. By completeness, to prove $$\vdash \forall v \Big [ \big [ \exists x M(x,v) \land \varphi_1^{M, E}(v) \land \cdots \land \varphi_n^{M, E}(v) \big ] \to \psi^{M,E}(v) \Big],$$ it suffices to show that this sentence is true in all $L$-structures.
So let $(U,\varepsilon)$ be an arbitrary $L$-structure. Let $c\in U$ be arbitrary. We must show $$U\models \big [ \exists x M(x,c) \land \varphi_1^{M, E}(c) \land \cdots \land \varphi_n^{M, E}(c) \big ] \to \psi^{M,E}(c).$$ So we may assume $U\models \exists x M(x,c) \land \varphi_1^{M, E}(c) \land \cdots \land \varphi_n^{M, E}(c)$ and show $U\models \psi^{M,E}(c)$. Since $U\models \exists x M(x,c)$, $M_c$ is non-empty, so $(M_c,E_c)$ is an $L$-structure. Since $U\models \varphi_i^{M,E}(c)$ for all $i$, $M_c\models \varphi_i$ for all $i$. Now since $\varphi_1,\dots, \varphi_n\models \psi$, $M_c\models \psi$, and therefore $U\models \psi^{M,E}(c)$.