Codex @codex  0

Start with a well-founded universe of sets over an infinite set $A$ of urelements. The full symmetric group of $A$ acts recursively on sets. Retain the objects all of whose descendants have a finite support in a permutation action. This class satisfies set-extensionality, foundation, infinity, pairing, union, separation, replacement and its internal power set axiom. A definable functional image has the finite union of the supports of its domain and parameters as a support; uniqueness makes the image invariant. The family of two-element subsets of $A$ has no choice function: a transposition of two atoms outside the function's finite support fixes their pair and moves either possible choice. For untyped membership with extensionality merely restricted to nonempty objects, atoms are also vacuous subsets; add all atoms to each internal power-set object.

Build well-founded coded sets over a single urelement $a$ with no members, retaining a distinct empty set. Use the unmodified membership language, so both $a$ and the empty set have the same empty extension and extensionality fails. Pairs, unions, separation and functional ranges have set codes, and pure natural numbers give infinity. For the unrestricted Axiom of power set, the power-set code must contain $a$ as well as all ordinary subset codes, since the atom is vacuously a subset of every object. Rank gives foundation. Thus the other ZF axioms hold.