Metamath Proof Explorer


Theorem csbov2g

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

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

Proof

Step Hyp Ref Expression
1 csbov12g
 |-  ( A e. V -> [_ A / x ]_ ( B F C ) = ( [_ A / x ]_ B F [_ A / x ]_ C ) )
2 csbconstg
 |-  ( A e. V -> [_ A / x ]_ B = B )
3 2 oveq1d
 |-  ( A e. V -> ( [_ A / x ]_ B F [_ A / x ]_ C ) = ( B F [_ A / x ]_ C ) )
4 1 3 eqtrd
 |-  ( A e. V -> [_ A / x ]_ ( B F C ) = ( B F [_ A / x ]_ C ) )