Metamath Proof Explorer

Theorem csbaovg

Description: Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion csbaovg 
|- ( A e. D -> [_ A / x ]_ (( B F C )) = (( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C )) )

Proof

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