From Dana Scott: More on the axiom of extensionality, in Essays on the foundations of mathematics, dedicated to A. A. Fraenkel on his seventieth anniversary, edited by Y. Bar-
Hillel, E. I. J. Poznanski, M. O. Rabin, and A. Robinson for The Hebrew University of Jerusalem, Magnes Press, Jerusalem 1961, pp. 115–131.
On page 118, Scott introduces the following three definitions:
$a\overset{=}{.}b\leftrightarrow\forall x(x\in a\leftrightarrow x\in b)$
$\mathbb{I}(a)\leftrightarrow\forall x,y(x\in a\wedge x\overset{=}{.}y\to y\in a)$
$\mathbb{H}(a)\leftrightarrow\mathbb{I}(a)\wedge\exists x(a\subseteq x\wedge \forall y(y\in x\to \mathbb{I}(y)\wedge y\subseteq x))$
A set $a$ is ext-invariant just if $\mathbb{I}(a)$, and hereditarily ext-invariant just if $\mathbb{H}(a)$.
Axiom of extensionality is (I), finite union is (II), infinite union (III), power set (IV), infinity (V), subsets (VI), replacement (VII).
$ZF^{\not =}$ is (II) to (VII).
On page 130 Scott writes:
"What would happen if (VII) [replacement, in $ZF^{\not =}$] were replaced by (VII')
$\forall x,y,z[\Phi(x,y)\wedge \Phi(x,z)\to x\overset{=}{.}y]\to\exists w\forall y[y\in w\leftrightarrow\exists x[x\in a\wedge\Phi(x,y)]] \ldots ?$
The theory based on (II) to (VI) and (VII') is certainly intermediate between $ZF^{\not =}$ and $ZF$. It is in fact much stronger than$ZF^{\not =}$, for it is possible to prove in this theory the statement
$\mathbb{I}(a)\wedge\forall x(x\in a\to\mathbb{H}(x))\to \mathbb{H}(a)$
Using this formula together with (VII') the method of Section 2 can be applied directly to show that $ZF$ is indeed interpretable in this new theory."
Let $ZF-$ be Scott's system based upon (II)-(VI) and (VII').
How did Scott prove his statement in $ZF-$?
Update: The satisfactory x, $a\subseteq x$, can be constructed as the $\overset{=}{.}$-adjusted transitive closure of $a$.
Best Answer
Retain the definitions in the question and let $Fn(f)$ express that $f$ is a function, $Dn(f)$ be the domain of function $f$ and $\omega$ be the set of natural numbers. Let $e\in^1 c\leftrightarrow e\in c $ and $e\in^{n+1}c\leftrightarrow\exists d(d\in^1c\wedge e\in^n d)$.
We define the $\overset{=}{.}$ -adjusted transitive closure of $a$ by means of (VII'):
$TC^{\overset{=}{.}}(a)=\{v|\exists w\exists x\exists y(\exists z(z\in\omega\wedge\exists f ( Fn(f) \wedge Dn(f)=z\cup\{z\}\land f(\emptyset)=\{a\}\\ \wedge (\forall n< z\to f(n\cup\{n\})=\bigcup f(n))\land (z,y)\in f\wedge x\in y\wedge w\in x\wedge v \overset{=}{.} w)\}$
We want to prove that $\mathbb{I}(a)\wedge\forall x(x\in a\to\mathbb{H}(x))\to \mathbb{H}(a)$, and suppose that $\mathbb{I}(a)\wedge\forall x(x\in a\to\mathbb{H}(x))$.
Clearly $a\subseteq TC^{\overset{=}{.}}(a)$. If $c\in TC^{\overset{=}{.}}(a)$, for some $n\in \omega: \exists b(b\overset{=}{.}c\wedge b\in ^n a)$. As the members of $a$ are hereditarily ext-invariant, i.e. $\forall x(x\in a\to\mathbb{H}(x))$, it follows that $\forall y(y\in TC^{\overset{=}{.}}(a)\to \mathbb{I}(y)\wedge y\subseteq TC^{\overset{=}{.}}(a)))$. So $\mathbb{H}(a)$, and we are done.