Description: Move class substitution in and out of a function value. (Contributed by NM, 10-Nov-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | csbfv2g | |- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( F ` [_ A / x ]_ B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbfv12 | |- [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) |
|
2 | csbconstg | |- ( A e. C -> [_ A / x ]_ F = F ) |
|
3 | 2 | fveq1d | |- ( A e. C -> ( [_ A / x ]_ F ` [_ A / x ]_ B ) = ( F ` [_ A / x ]_ B ) ) |
4 | 1 3 | eqtrid | |- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( F ` [_ A / x ]_ B ) ) |