 Let us pause to discuss this important technique. Suppose &lt; M, E&gt; is a well-founded model of the axiom of extensionality. It is a consequence of the well-foundedness of the binary predicate E on M, and of the principle of transfinite recursion, that the equation π(x) = {π(y) | y ∈ M ∧ yEx} defines a unique function on M. The range N of π is transitive, for if π(a) ∈ N and y ∈ π(a), then y = π(b) for some b ∈ M with bEa, whence π(b) ∈ N. The fact that π is an isomorphism between &lt; M, E&gt; and &lt; N, ∈ &gt; can be proved by transfinite induction on elements on M, based again on the well-foundedness of E. The well-foundedness of &lt; M, E&gt; is in practice often the consequence of &lt; M, E&gt; being a submodel of some &lt; Vα, ε &gt;.