Description: Part of a study of the Axiom of Replacement used by the Isabelle prover.
The object PrimReplace is apparently the image of the function encoded
by ph ( x , y ) i.e. the class ( { <. x , y >. | ph } " A ) .
If so, we can prove Isabelle's "Axiom of Replacement" conclusion without
using the Axiom of Replacement, for which I (N. Megill) currently have
no explanation. (Contributed by NM, 26-Oct-2006)(Proof shortened by Mario Carneiro, 4-Dec-2016)(Proof shortened by SN, 19-Dec-2024)