Skolem hulls are small elementary substructures

By F5 and A1 fix a well-order of $M$. Its least element is $m_0$; selecting the least satisfying element of each nonempty existential witness set, and $m_0$ otherwise, gives the family of F1. The same remaining argument applies to any already supplied family. This is the use of choice needed to produce witnesses for an arbitrary structure.

The alphabet consisting of the nonlogical symbols, countably many variables and finitely many punctuation/constructor tokens has size at most $\kappa$, by F4. Fix an injection of it into $\kappa$ and a pairing injection ${\kappa }^2\to \kappa$ from F3. Recursively pairing coordinates gives injections ${\kappa }^n\to \kappa$ for each positive finite $n$; the empty word is one additional element. Encoding the length as well gives an injection of all finite words into $\omega \times \kappa$, of size $\kappa$ by F4. Formulas are particular finite words, so there are at most $\kappa$ formulas and at most $\kappa$ pairs $(x,\psi )$. Thus there are at most $\kappa$ closure operations in F1, all of finite arity.

If $\mathrm{\mid }{H}_n\mathrm{\mid }\le \kappa$, the same finite-tuple encoding gives at most $\kappa$ tuples of each arity and at most $\kappa$ operation/tuple pairs in total. Their image has size at most $\kappa$: well-order the pair codes and assign to each image element its least preimage code. Adding $H_n$ and the at most $\kappa$ constants preserves the bound by F4. Also $\mathrm{\mid }{H}_0\mathrm{\mid }=\mathrm{\mid }A\cup \{m_0\}\mathrm{\mid }\le \kappa$. Induction proves $\mathrm{\mid }{H}_n\mathrm{\mid }\le \kappa$ for all $n$. To bound the union, use A1 on the nonempty sets of injections $H_n\to \kappa$, obtaining injections $j_n$ simultaneously. Assign $a\in H$ the pair $(n,j_n(a))$ for its least membership stage $n$. This injects $H$ into $\omega \times \kappa$, giving $\mathrm{\mid }H\mathrm{\mid }\le \kappa$ by F4. This explicitly accounts for the countable choice in this union bound.

The hull contains $m_0$ and every constant. A finite tuple in $H$ lies in a common $H_n$: take the maximum of its finitely many membership stages, using $n=0$ for the empty tuple. Applying an original function sends it into $H_{n+1}$. Hence the restricted structure on $H$ is a nonempty substructure. For a true existential instance with parameters in $H$, put its parameter tuple in $H_n$ in the same way. The corresponding witness value belongs to $H_{n+1}$ and satisfies the matrix in $\mathcal{M}$, by F1. F2 now gives $H\prec \mathcal{M}$. Taking $\kappa ={\mathrm{\aleph }}_0$ gives the countable assertion, with the same choice uses; it is not a claim of a choice-free countable hull for arbitrary $M$.