Rieger-Bernays permutation model ($xEy⟺x\in \pi (y)$)

A definable class bijection $\pi$ of a model's universe changes membership as displayed. Images and inverse images of sets under $\pi$ remain sets by the Axiom schema of replacement. The new extension of $y$ is the old set $\pi (y)$. Thus the representative of any desired extension $b$ is ${\pi }^{-1}(b)$. Extensionality follows from bijectivity; separation and replacement translate to old definable formulas; pairs, unions and power sets have explicit representatives. Infinity follows by iterating the new empty set and successor. Foundation need not survive: interchanging $\varnothing$ and $\{\varnothing \}$ makes the old empty set a Quine atom. A full such permutation of a model of choice still satisfies choice; failure of choice requires an additional symmetry restriction.

A Quine atom is a set whose sole member is itself. It violates the Axiom of foundation while respecting the axiom of extensionality. Swapping pairwise distinct old objects $a_n$ with their singletons in a Rieger-Bernays permutation model supplies many Quine atoms, provided those transpositions have disjoint supports. For example, the old ordinals $a_n=\omega +n$ and their singletons are disjoint families.

Start with distinct formal atoms $q\in A$ with membership extensions $\{q\}$. Recursively adjoin a unique representative $S(X)$ of every subset $X$ of a previous stage, except that $S(\{q\})=q$ uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.

Build the cumulative universe over an infinite set $A$ of Quine atoms, and extend every permutation of $A$ recursively to its other sets. An object has finite support if every permutation fixing that finite subset of $A$ fixes the object. Retain objects whose members, recursively away from the atomic self-loops, also have finite support. Parameters and domains give finite supports for definable subsets and functional ranges; the collection of all retained subsets of a retained set is again supported. These observations verify separation, replacement and power set, and the pure natural-number hierarchy gives infinity. There is no choice function on the two-element subsets of $A$: swap two atoms outside its supposed finite support, fixing their unordered pair but interchanging either possible selected member.