I am not sure if this is relevant, but here it is. Formally speaking, ZF is a first-order theory. It includes axioms of classical logic, properly ZF axioms, and rules of inference. A proof in ZF is a mathematical object: a sequence or a tree built from formulas and arranged according to the rules of inference.i) a,b,c ordinals. Derive the following cancellation law: a+b=a+c implies b=c.
I can show this by induction, but I don't think that comes under the heading of "derive". How can this be derived from axioms/ definitions etc?
That said, in practice one cannot build formal proofs by hand of any but the simplest statement. From some point one starts "reasoning within the theory". E.g., instead of applying a disjunction elimination rule to three formulas, one just does informal reasoning by cases. The idea is that first-order logic describes mathematical reasoning so well that one adopts an informal principle: everything that can be deduced informally can be formalized and presented as a formal derivation.
Now, if I remember correctly, transfinite induction is a theorem whose proof from axioms can also be formalized. Therefore, one can use it and call it "deriving".
You may know all this, and the answer to your question may depend on the course context. Sometimes the problem asks for a formal derivation. I just wanted to say that, ultimately, induction has a formal proof from axioms like any other theorem.