Can full replacement follow from well ordered replacement over rest of axioms of ZF? Would axiom schema of Replacement follow from well-ordered Replacement?
What I mean is that if we restrict Replacement to only well ordered sets, then can that still prove full Replacement?
Well ordered Replacement is the axiom schema stating that for every set $A$ that admits a well ordering on it, and for every definable function $f$ [not using the symbol $B$], there exists the set $B=\{f(x): x \in A \}$.
So can $\sf ZF\text{-Replacement+Well ordered Replacement} \vdash Replacement$
I think well ordered replacement is of the same consistency strength of full replacement, but can it prove it??
 A: We will show that replacement is provable in Zermelo set theory plus foundation plus well ordered replacement.
(1) Suppose $a$ is a set , $F$ is a formula, and for every $x \in a$ there is a unique $y$ such that $F(x,y)$. Suppose that if $x \in a$ and $F(x,y)$, then $y \in V_\beta$ for some ordinal $\beta$. Then there is a set $b$ such that
$y \in b \iff \exists x \in a : F(x,y)$
Proof: Define an equivalence relation W on a by (r,s)∈W iff (for all ordinals β, if Vβ exists, F(r,r') and F(s,s') then r'∈Vβ<-->s'∈Vβ). Define an ordering on the equivalence classes of W by [r]<[s] iff there
is an ordinal β  such that r'∈Vβ  and s'∉Vβ where F(r,r') and F(s,s'). The equivalence classes of W are well-ordered by this ordering. Let G(u,v) be the formula
"there is an x∈a such that u=[x], F(x,y), β is the least ordinal such  that y∈Vβ, and v=Vβ. By well ordered replacement there is a set c such that
v∈c<-->(G(u,v) for some u in the set of equivalence classes of W).LetY=Uc.
Then b={y∈Y|F(x,y) for some x∈a}
(2)For every x there is an ordinal β such that x∈Vβ.
Proof:Suppose that this is not true and that c is not in Vβ for any ordinal β. By well ordered replacement there is a set d which is the transitive closure of c. Let s={x∈dU{c}| x∉Vβ for any ordinal β}.
By foundation there is t∈s such that t intersect s is empty.Let F(x,y) be the formula "y is the least Vα  with x∈Vα". By (1), there is a set b such that y∈b<-->(F(x,y) for some x∈t). Then
  t is in the power set of Ub. This contradicts our assumption about t.

Replacement follows from (1) and (2).
