Metamath Proof Explorer


Theorem tfrlem3

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

Ref Expression
Hypothesis tfrlem3.1 A=f|xOnfFnxyxfy=Ffy
Assertion tfrlem3 A=g|zOngFnzwzgw=Fgw

Proof

Step Hyp Ref Expression
1 tfrlem3.1 A=f|xOnfFnxyxfy=Ffy
2 vex gV
3 1 2 tfrlem3a gAzOngFnzwzgw=Fgw
4 3 eqabi A=g|zOngFnzwzgw=Fgw