Metamath Proof Explorer

Theorem csbrecsg

Description: Move class substitution in and out of recs . (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbrecsg 
|- ( A e. V -> [_ A / x ]_ recs ( F ) = recs ( [_ A / x ]_ F ) )

Proof

Step Hyp Ref Expression
1 csbwrecsg 
 |-  ( A e. V -> [_ A / x ]_ wrecs ( _E , On , F ) = wrecs ( [_ A / x ]_ _E , [_ A / x ]_ On , [_ A / x ]_ F ) )
2 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ _E = _E )
3 wrecseq1 
 |-  ( [_ A / x ]_ _E = _E -> wrecs ( [_ A / x ]_ _E , [_ A / x ]_ On , [_ A / x ]_ F ) = wrecs ( _E , [_ A / x ]_ On , [_ A / x ]_ F ) )
4 2 3 syl 
 |-  ( A e. V -> wrecs ( [_ A / x ]_ _E , [_ A / x ]_ On , [_ A / x ]_ F ) = wrecs ( _E , [_ A / x ]_ On , [_ A / x ]_ F ) )
5 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ On = On )
6 wrecseq2 
 |-  ( [_ A / x ]_ On = On -> wrecs ( _E , [_ A / x ]_ On , [_ A / x ]_ F ) = wrecs ( _E , On , [_ A / x ]_ F ) )
7 5 6 syl 
 |-  ( A e. V -> wrecs ( _E , [_ A / x ]_ On , [_ A / x ]_ F ) = wrecs ( _E , On , [_ A / x ]_ F ) )
8 1 4 7 3eqtrd 
 |-  ( A e. V -> [_ A / x ]_ wrecs ( _E , On , F ) = wrecs ( _E , On , [_ A / x ]_ F ) )
9 df-recs 
 |-  recs ( F ) = wrecs ( _E , On , F )
10 9 csbeq2i 
 |-  [_ A / x ]_ recs ( F ) = [_ A / x ]_ wrecs ( _E , On , F )
11 df-recs 
 |-  recs ( [_ A / x ]_ F ) = wrecs ( _E , On , [_ A / x ]_ F )
12 8 10 11 3eqtr4g 
 |-  ( A e. V -> [_ A / x ]_ recs ( F ) = recs ( [_ A / x ]_ F ) )