The main difficulty with the Replacement Axiom is that of how to formulate the notion of a functional correspondence. This was not solved satisfactorily by Fraenkel, but the Weyl/Skolem solution works here, too: a functional correspondence is (in effect) just any first-order 2-place predicate ϕ(x, y) which satisfies the condition of uniqueness, i.e., ∀x, y, z{[ϕ(x, y) ∧ ϕ(x, z)] → y = z}. With this solution, the Replacement Axiom will be (as required) stronger than Zermelo's original Separation Axiom and indeed can replace it; however, in Fraenkel's system, one can prove his version of the Replacement Axiom from his version of the Separation Axiom, which shows that his separate definition of function is not sufficiently strong. (For details, see Hallett 1984: 282–286.)