 Non-extensional membership model with one atom

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.