Finite-tuple satisfaction is absolute

Fix an actual formula code and take $m\in \omega$ greater than every variable index occurring anywhere in it, including bound indices. Transitivity and internal Pairing and Union put every finite tuple from $A$ in $N$. Conversely every internal $m$-tuple from $A$ is an actual one: the domain, entries and ordered pairs agree by transitivity. Finite code parsing uses the same finite words in both universes.

On each subformula define truth for assignments $t\in A^m$ recursively. For atoms use equality or membership of the indicated coordinates; use complement and intersection for negation and conjunction; for $\mathrm{\exists }{v}_i\psi$ use $\mathrm{\exists }b\in A$ applied to the truth of $\psi$ at $t[i:=b]$. Recursion into $\mathcal{P}(A^m)$ is a set construction, both internally and externally.

Constructor induction identifies these truth values. Atoms compare the same sets by the same membership relation. Equal child truth values give equal negations and conjunctions. At an existential node each witness on either side lies in the identical set $A$, and its updated tuple is in $N$ by step 1.1; the induction hypothesis therefore transfers each witness in both directions. This comparison does not require equality of the internal and external power sets of $A^m$.

Fix one $a_0\in A$. An $m$-tuple extends to an infinite assignment by setting every later coordinate equal to $a_0$; Replacement constructs this extension inside $N$ as well as outside. The satisfaction clauses show by constructor induction that this extension has exactly the recursively computed finite truth values. Coincidence makes all choices of extension equivalent on the free variables. Step 3.1 thus proves the asserted equality of internal and external satisfaction for every finite tuple. The single choice of $a_0$ is existential instantiation, not AC.