Mostowski collapse ($\pi (x)=\{\pi (y):yRx\}$)

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.