Metamath Proof Explorer

Theorem csbov123

Description: Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005) (Revised by NM, 23-Aug-2018)

Ref Expression
Assertion csbov123 
|- [_ 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 oveq123d 
 |-  ( 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 nfov 
 |-  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 oveq123d 
 |-  ( 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. _V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) )
18 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B F C ) = (/) )
19 df-ov 
 |-  ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) = ( [_ A / x ]_ F ` <. [_ A / x ]_ B , [_ A / x ]_ C >. )
20 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ F = (/) )
21 20 fveq1d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ F ` <. [_ A / x ]_ B , [_ A / x ]_ C >. ) = ( (/) ` <. [_ A / x ]_ B , [_ A / x ]_ C >. ) )
22 0fv 
 |-  ( (/) ` <. [_ A / x ]_ B , [_ A / x ]_ C >. ) = (/)
23 21 22 eqtrdi 
 |-  ( -. A e. _V -> ( [_ A / x ]_ F ` <. [_ A / x ]_ B , [_ A / x ]_ C >. ) = (/) )
24 19 23 eqtr2id 
 |-  ( -. A e. _V -> (/) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) )
25 18 24 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) )
26 17 25 pm2.61i 
 |-  [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C )