Metamath Proof Explorer

Theorem csbafv212g

Description: Move class substitution in and out of a function value, analogous to csbfv12 , with a direct proof proposed by Mario Carneiro, analogous to csbov123 . (Contributed by AV, 4-Sep-2022)

Ref Expression
Assertion csbafv212g 
|- ( A e. V -> [_ A / x ]_ ( F '''' B ) = ( [_ A / x ]_ F '''' [_ A / x ]_ B ) )

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( F '''' B ) = [_ A / x ]_ ( F '''' B ) )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ F = [_ A / x ]_ F )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
4 2 3 afv2eq12d 
 |-  ( y = A -> ( [_ y / x ]_ F '''' [_ y / x ]_ B ) = ( [_ A / x ]_ F '''' [_ A / x ]_ B ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( F '''' B ) = ( [_ y / x ]_ F '''' [_ y / x ]_ B ) <-> [_ A / x ]_ ( F '''' B ) = ( [_ A / x ]_ F '''' [_ A / x ]_ B ) ) )
6 vex 
 |-  y e. _V
7 nfcsb1v 
 |-  F/_ x [_ y / x ]_ F
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
9 7 8 nfafv2 
 |-  F/_ x ( [_ y / x ]_ F '''' [_ y / x ]_ B )
10 csbeq1a 
 |-  ( x = y -> F = [_ y / x ]_ F )
11 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
12 10 11 afv2eq12d 
 |-  ( x = y -> ( F '''' B ) = ( [_ y / x ]_ F '''' [_ y / x ]_ B ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( F '''' B ) = ( [_ y / x ]_ F '''' [_ y / x ]_ B )
14 5 13 vtoclg 
 |-  ( A e. V -> [_ A / x ]_ ( F '''' B ) = ( [_ A / x ]_ F '''' [_ A / x ]_ B ) )