Uniform diagonal lemma

Statement

Let $\psi (x, y_1, \dots , y_n)$ be any formula with free variables $x, y_1, \dots , y_n$.

Then there is a formula $\varphi (y_1, \dots y_n)$ with free variables $y_1, \dots , y_n$ such that for all $m_1 , \dots , m_n \in \mathbb{N}$, $T \vdash \varphi (\overline{m_1} , \dots , \overline{m_n}) \leftrightarrow \psi (\ulcorner \varphi (\overline{m_1} , \dots , \overline{m_n}) \urcorner, \overline{m_1} , \dots , \overline{m_n})$.