Metamath Proof Explorer


Theorem csbafv12g

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 Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion csbafv12g A 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 afveq12d 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 V
7 nfcsb1v _ x y / x F
8 nfcsb1v _ x y / x B
9 7 8 nfafv _ 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 afveq12d 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 V A / x F ''' B = A / x F ''' A / x B