Mostowski collapse theorem

Every well-founded extensional relation is uniquely isomorphic to membership on a transitive set.

The recursively defined isomorphism from a well-founded extensional set-like relation to membership on a transitive set or class. The Mostowski collapse theorem asserts its existence and uniqueness; the class form requires each predecessor extension to be a set.

If $X$ has a well-founded extensional inherited membership relation and $T\subseteq X$ is a transitive set, its Mostowski collapse theorem map $\pi$ fixes every member of $T$. The recursion $\pi (x)=\{\pi (y):y\in x\cap X\}$ and well-founded relation induction give this pointwise. If also $T\in X$, then $\pi (T)=T$.