Non-extensional membership model with one atom (source code)

= 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.