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 e. 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 e. V -> [_ A / x ]_ frecs ( R , D , ( F o. 2nd ) ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ ( F o. 2nd ) ) )
2 eqid 
 |-  [_ A / x ]_ R = [_ A / x ]_ R
3 eqid 
 |-  [_ A / x ]_ D = [_ A / x ]_ D
4 csbcog 
 |-  ( A e. V -> [_ A / x ]_ ( F o. 2nd ) = ( [_ A / x ]_ F o. [_ A / x ]_ 2nd ) )
5 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ 2nd = 2nd )
6 5 coeq2d 
 |-  ( A e. V -> ( [_ A / x ]_ F o. [_ A / x ]_ 2nd ) = ( [_ A / x ]_ F o. 2nd ) )
7 4 6 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ ( F o. 2nd ) = ( [_ A / x ]_ F o. 2nd ) )
8 frecseq123 
 |-  ( ( [_ A / x ]_ R = [_ A / x ]_ R /\ [_ A / x ]_ D = [_ A / x ]_ D /\ [_ A / x ]_ ( F o. 2nd ) = ( [_ A / x ]_ F o. 2nd ) ) -> frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ ( F o. 2nd ) ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , ( [_ A / x ]_ F o. 2nd ) ) )
9 2 3 7 8 mp3an12i 
 |-  ( A e. V -> frecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ ( F o. 2nd ) ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , ( [_ A / x ]_ F o. 2nd ) ) )
10 1 9 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ frecs ( R , D , ( F o. 2nd ) ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , ( [_ A / x ]_ F o. 2nd ) ) )
11 df-wrecs 
 |-  wrecs ( R , D , F ) = frecs ( R , D , ( F o. 2nd ) )
12 11 csbeq2i 
 |-  [_ A / x ]_ wrecs ( R , D , F ) = [_ A / x ]_ frecs ( R , D , ( F o. 2nd ) )
13 df-wrecs 
 |-  wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) = frecs ( [_ A / x ]_ R , [_ A / x ]_ D , ( [_ A / x ]_ F o. 2nd ) )
14 10 12 13 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ wrecs ( R , D , F ) = wrecs ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ F ) )