Metamath Proof Explorer

Theorem csbov

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

Ref Expression
Assertion csbov 
|- [_ A / x ]_ ( B F C ) = ( B [_ A / x ]_ F C )

Proof

Step Hyp Ref Expression
1 csbov123 
 |-  [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C )
2 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ B = B )
3 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ C = C )
4 2 3 oveq12d 
 |-  ( A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) = ( B [_ A / x ]_ F C ) )
5 0fv 
 |-  ( (/) ` <. B , C >. ) = (/)
6 df-ov 
 |-  ( B (/) C ) = ( (/) ` <. B , C >. )
7 0ov 
 |-  ( [_ A / x ]_ B (/) [_ A / x ]_ C ) = (/)
8 5 6 7 3eqtr4ri 
 |-  ( [_ A / x ]_ B (/) [_ A / x ]_ C ) = ( B (/) C )
9 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ F = (/) )
10 9 oveqd 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) = ( [_ A / x ]_ B (/) [_ A / x ]_ C ) )
11 9 oveqd 
 |-  ( -. A e. _V -> ( B [_ A / x ]_ F C ) = ( B (/) C ) )
12 8 10 11 3eqtr4a 
 |-  ( -. A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) = ( B [_ A / x ]_ F C ) )
13 4 12 pm2.61i 
 |-  ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C ) = ( B [_ A / x ]_ F C )
14 1 13 eqtri 
 |-  [_ A / x ]_ ( B F C ) = ( B [_ A / x ]_ F C )