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 ) ) |
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 ) ) |