Does ZFC prove every extensional well-founded out-tree translate into a set? Let $T$ be an extensional well-founded out-tree, where well-founded refers to absence of infinite branches, and extensional refers to absence of two isomorphic full subtrees of $T$ whose root nodes are connected to a common node in $T$. By full subtree of $T$ its meant a subtree of $T$ that has every branch of $T$ stemming from its root node being a branch of it! For any node $n$ in $T$ we call the full subtree of $T$ stemming from it as $Tree^T(n)$
We define a translation function $f$ from nodes of $T$ to a set $x$ as:
$f(root( T)) = x \\ f(n)=f(m) \iff Tree^T(n) \approx Tree^T(m)$
Where $\approx$ stand for isomorphism between trees.
Now we define a graph $G(f)$ on $range(f)$ that has a directed edge between any elements of $range(f)$ if and only if an element of the pre-image (under $f$) of one of them is connected by an edge to an element of the pre-image (under $f$) of the other node, and the direction of that edge in $G(f)$ is the same as that between those two connected nodes in $T$.
Now $f$ would be called a translation from tree $T$ to set $x$ if and only if $G(f)$ is the membership relation on the transitive closure set of $x$.
So we'd say: a tree $T$ translates into a set $x$ if and only if a translation $f$ exists between them.

Does $\sf ZFC$ prove that "every extensional well-founded out-tree translates into a set"?


If we add the above as an axiom to $\sf ZF$, would that get to interpret  $\sf AC$?


Every extensional and well-founded relation on a set is isomorphic to a unique transitive set. This is the set-version of Mostowski's collapse lemma (the general version on classes requires that the relation is also set-like: every point has only a set that is "in relation with it", e.g. the class of ordinals and the transitive set is now a transitive class).
So $\sf ZF$ proves that every extensional and well-founded tree is isomorphic to a set. Therefore your questions are answered yes and no respectively.
