Definable subsets of a membership structure

Work in ZF. If $A\mathrm{\ne }\mathrm{\varnothing }$, define

$\mathrm{Def}(A)=\{\{x\in A:(A,\in )\models \varphi (x,a_1,\dots ,a_n)\}:n<\omega ,a\in A^n,\mathrm{FV}(\varphi )\subseteq \{v_0,\dots ,v_n\}\}\mathrm{.}$

Here $x$ is assigned to $v_0$ and $a_i$ to $v_i$; unused variables are allowed. Use the finite-tuple satisfaction convention of Finite-tuple satisfaction is absolute. Formula codes and finite tuples form a set. Separation produces the uniquely specified subset for each pair of code and tuple, and Replacement collects their values; hence $\mathrm{Def}(A)$ is a set contained in $\mathcal{P}(A)$, uniformly definable from $A$.

Set $\mathrm{Def}(\mathrm{\varnothing })=\{\mathrm{\varnothing }\}$ separately. This avoids treating the empty carrier as a first-order structure. Empty parameter tuples give parameter-free definitions. Parameters need not be distinct. Only satisfaction for a set structure is used; no truth predicate for the universe is asserted.