ZFA universes, atoms, pure sets, and the kernel

A ZFA universe has a distinguished set $A$ of atoms. An atom has no members but is not the empty set; Extensionality is restricted to non-atoms, while Pairing, Union, Power Set, Separation, Replacement, Infinity and Foundation have their usual set clauses. Define

$V_0(A)=A,V_{\alpha +1}(A)=V_{\alpha }(A)\cup \mathcal{P}(V_{\alpha }(A)),V_{\lambda }(A)={\bigcup }_{\alpha <\lambda }{V}_{\alpha }(A)\mathrm{.}$

The ZFA universe is generated by ${\bigcup }_{\alpha }{V}_{\alpha }(A)$. An object $x$ is pure if it is a set (not an atom) and the transitive closure of the singleton $\{x\}$ contains no atom; equivalently, neither $x$ nor anything recursively belonging to $x$ is an atom. The singleton is essential here because, under the convention of Transitive closure of a set, $\mathrm{TC}(x)$ need not contain $x$ itself. The class of pure sets, the kernel, is the hierarchy generated from $\mathrm{\varnothing }$ and is a transitive ZF model: rank induction identifies each pure stage with the ordinary cumulative hierarchy and the ZFA set axioms restrict to it. This kernel conclusion is choice-free. If the ambient ZFA universe satisfies AC, applying an ambient choice function to any pure family yields a pure graph, so the kernel satisfies AC as well; this optional restriction is the exact use of The Axiom of Choice.