A question about equivalence of well-foundedness notions and if they beg a form of choice? Take these three notions for well founded sets:
[1] A well founded set is one that is not an element of any descending membership set.
[2] A well founded set is one where every nonempty subset of its transitive closure has an element that is disjoint of it.
[3] A well founded set is a subset of a stage of the cumulative hierarchy.
Formally speaking:
[1] $WF(x) \leftrightarrow \forall y (\forall b \in y \exists a \in y \, (a \in b) \to x \not \in y) $
[2] $WF(x) \iff \forall c \neq \emptyset \, (c \subseteq \text{tcl}(x) \to \exists y \in c \,( y \cap c = \emptyset)) $
[3] $WF(x) \iff \exists \alpha: x \in V_\alpha$
[Note]: a descending membership set here means a set having no minimal member, that is: a set whose elements are not disjoint of it.

Do we need a form of choice to establish the equivalence between some two of these definitions (especially 1 and 2) over axioms of $\sf ZF - Reg.$? or over axioms of $\sf Z$?

 A: I think that All three are equivalent in ZF-Regularity without any need for DC.
I'll label those definition by $ WF^1, WF^2, WF^3$ to be the notions defined by the repsective statements mentioned above.
Proof of $\forall x: WF^1(x) \iff WF^2(x)$:
For ease lets take their negation, that is
$\forall x: \neg WF^1(x) \iff \neg WF^2(x)$
For the left to right direction, since there is a set $y$ in which all of its elements are not disjoint of it, that has $x$ among its elements, then $y \cap \text{tcl}(x)$ is nonempty and also has all of its elements being not disjoint of it, thus $\neg WF^2(x)$
For the right to left direction, define a new binary relation "higher than", denoted by $``>^*"$, as: $$ x >^* y \iff y \in \text{tcl}(x)$$
Since we have $\neg WF^2(x)$, then there exists a nonempty subset $c$ of $\text{tcl}(x)$, having all of its elements being not disjoint of it.
Now take the set $H$ of all elements of $\text{tcl}(x)$ that are higher than elements of $c$; that is: $$H=\{y \in \text{tcl}(x) \mid \exists m \in c \,(y >^* m) \}$$, and clearly $\{x\} \cup H$ would have all of its elements being not disjoint of it!
Proof of $\forall x: \neg WF^3 \iff \neg WF^1$
To prove that we need to first prove that for every set $x$ if every element $y$ of $x$ is an element of some $V_\alpha$, then $x$ itself is an element of some $V_\lambda$. The proof is easy, we first prove that there exists a set of all equivalence classes of elements of $x$ under equivalence relation "have the same ranks", this is easily provable from Power set axiom and Separation. Now that set would be equal in size with the class of all ranks of elements of $x$, thus by Replacement, there is a set of all those ranks and its union is just another rank of which $x$ is a subset and thus an element of its successor rank. Now $\in$-induction will work over the cumulative hierarchy portion of the world of $\sf ZF$-Reg., because its stages are indexed with ordinals which are built-in well founded sets. So, its easy to prove that any set outside the cumulative hierarchy won't be well founded along any of definitions 1 or 2, and with $\in$- induction over the cumulative hierarchy its easy to prove that all sets in it would satisfy definitions 1 and 2.
For the equivalence over Zermelo, it appears that 1 and 2 equivalence requires transitive closures, so $\sf Z + \forall x: \text{tcl}(x) \, exists $ seems to be adequate for a proof of that equivalence.
However, the equivalence with 3 uses Replacement, so they are not provably equivalent in $\sf Z$.
However, from the above proof, I think the least needed requirement to establish this equivalence in terms of theories extending $\sf Z$, is the theory: $$\sf Zermelo + Ranking + Transitiveness $$ The Ranking axiom is the statement that every set whose elements are elements of stages of the cumulative hierarchy, then it is an element of a stage of the cumulative hierarchy, formally that is:
Ranking: $\forall x: (\forall y \in x \, \exists \alpha: y \in V_\alpha) \to \exists \alpha: x \in V_\alpha$
The Transitiveness axiom is the statement that every set is a subset of a transitive set.
Transitiveness: $\forall x \, \exists y: trs(y) \land x \subseteq y$
Where: $trs(y) \iff \forall z \in y \,(z \subseteq y)$
