 Term-value formula in relational coding

After replacing functions by graph predicates and constants by singleton predicates, $E_t(z)$ says that $z$ is the value of a term $t$. For a unary function graph $P$ and constant predicate $Q$, use $E_x(z)=(z=x)$, $E_c(z)=Q(z)$ and $E_{f(t)}(z)=\exists y(E_t(y)\wedge P(y,z))$. Fresh witnesses avoid variable capture. Totality and uniqueness axioms make each value formula have exactly one witness under every assignment.