Metamath Proof Explorer


Theorem csbfv2g

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

Proof

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