Metamath Proof Explorer


Theorem csbwrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020) (Revised by Scott Fenton, 18-Nov-2024)

Ref Expression
Assertion csbwrecsg A V A / x wrecs R D F = wrecs A / x R A / x D A / x F

Proof

Step Hyp Ref Expression
1 csbfrecsg A V A / x frecs R D F 2 nd = frecs A / x R A / x D A / x F 2 nd
2 eqid A / x R = A / x R
3 eqid A / x D = A / x D
4 csbcog A V A / x F 2 nd = A / x F A / x 2 nd
5 csbconstg A V A / x 2 nd = 2 nd
6 5 coeq2d A V A / x F A / x 2 nd = A / x F 2 nd
7 4 6 eqtrd A V A / x F 2 nd = A / x F 2 nd
8 frecseq123 A / x R = A / x R A / x D = A / x D A / x F 2 nd = A / x F 2 nd frecs A / x R A / x D A / x F 2 nd = frecs A / x R A / x D A / x F 2 nd
9 2 3 7 8 mp3an12i A V frecs A / x R A / x D A / x F 2 nd = frecs A / x R A / x D A / x F 2 nd
10 1 9 eqtrd A V A / x frecs R D F 2 nd = frecs A / x R A / x D A / x F 2 nd
11 df-wrecs wrecs R D F = frecs R D F 2 nd
12 11 csbeq2i A / x wrecs R D F = A / x frecs R D F 2 nd
13 df-wrecs wrecs A / x R A / x D A / x F = frecs A / x R A / x D A / x F 2 nd
14 10 12 13 3eqtr4g A V A / x wrecs R D F = wrecs A / x R A / x D A / x F