Absoluteness of the definable power-set operation

If $A=\mathrm{\varnothing }$, internal Pairing constructs the actual singleton $\{\mathrm{\varnothing }\}$ by transitivity, so both Def operations give that set. Suppose henceforth that $A\mathrm{\ne }\mathrm{\varnothing }$.

For each external formula and finite parameter tuple from $A$, the code and tuple belong to $N$. Internal Separation gives $b\in N$ consisting of the internally satisfying elements of $A$. For each actual $x\in A$, finite-tuple absoluteness gives $x\in b$ exactly when the external formula holds. Transitivity ensures that $b$ has no additional elements. Hence every external Def subset is an internal Def subset.

Conversely an internal member of Def has an internal code and tuple witnessing its definition. These are actual code and tuple, and the same satisfaction comparison identifies its subset with the externally defined one. Internal Replacement collects exactly these subsets; both inclusions show equality of the two Def sets.