Urelement

An urelement is an object permitted alongside sets, with no members, distinguished from the empty set by an atom or set predicate. Extensionality is restricted to sets, so distinct atoms need not be equal merely because they have no members. An atom is different from a Quine atom, which is a set with a self-member. In simple typed set theory with atoms, each sort may contain urelements in addition to the objects representing subsets of the preceding sort.

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.