In the book Introduction to Set Theory 3rd ed. by Hrbacek and Jech one can find proofs of the following two theorems:
Transfinite Recursion Theorem. Let $G(x)$ be an operation. Then there exists an operation $F(x)$ such that $F(\alpha)=G(F\restriction\alpha)$ for all ordinals $\alpha$.
Transfinite Recursion Theorem, Parametric Version. Let $G(z,x)$ be an operation. Then there exists an operation $F(z,x)$ such that $F(z,\alpha)=G(z,F_z\restriction \alpha)$ for all ordinals $\alpha$ and all sets $z$.
where $F_z$ denotes the unary operation $F_z(x)=F(z,x)$.
The authors suggest to prove the second theorem by repeating the proof of the first one while carrying $z$ as a parameter troughout.
I was wondering if the following alternative proof is also valid:
The proof of the transfinite recursion theorem shows that the property defining $F$ can be written explicitly from the property defining $G$. Let $P(G)$ denote this property.
Let $G(z,x)$ be an operation. For any fixed $z$ let $G_z$ denote the operation defined by $G_z(x)=G(z,x)$. From the transfinite recursion theorem the property $P(G_z)$ defines an operation $F_z$ for each $z$.
Let $F$ be the operation defined by $F(z,x)=F_z(x)$. Then $F$ satisfies the desired properties.
Best Answer
If the proof of the first one doesn't let you carry $z$ as an extra parameter, then no, you can't do what you're suggesting. A property is described by a single formula of the language of set theory. You can't have a formula varying as a function of a set in the model unless that set is plugged in as an extra parameter in the formula. The theorem itself is really a theorem schema which takes the formula defining the property as input. The body of the proof then uses this formula to derive another formula to apply an instance of the Replacement axiom schema to. A proof is only allowed to use finitely many axioms of ZF/ZFC. This includes instantiating an axiom schema (comprehension, replacement) only finitely many times in a proof. So if the theorem is a schema that takes formulas as 'input', and then plugs the input formulas as subformulas into ZF axiom schemas, you're only allowed to take in finitely many formulas, and plug into axiom schemas finitely many times during a single instantiation of a proof. If you're familiar with C++ programming, using schemas is kind of like using templates in a C++ program.