Let $M$ be a countable transitive model of ZFC, let $\mathbb P \in M$, and let $\varphi(x_1,\dots,x_n)$ be a formula in the language of set theory. There is a relation, definable in $M$ from $\mathbb P$ and the Gödel code of $\varphi$, such that for all $p \in \mathbb P$ and all $\mathbb P$-names $\tau_1,\dots,\tau_n \in M$, the relation holds exactly when
\begin{align*}
p \Vdash \varphi(\tau_1,\dots,\tau_n).
\end{align*}