Metamath Proof Explorer

Theorem csbfv

Description: Substitution for a function value. (Contributed by NM, 1-Jan-2006) (Revised by NM, 20-Aug-2018)

Ref Expression
Assertion csbfv 
|- [_ A / x ]_ ( F ` x ) = ( F ` A )

Proof

Step Hyp Ref Expression
1 csbfv2g 
 |-  ( A e. _V -> [_ A / x ]_ ( F ` x ) = ( F ` [_ A / x ]_ x ) )
2 csbvarg 
 |-  ( A e. _V -> [_ A / x ]_ x = A )
3 2 fveq2d 
 |-  ( A e. _V -> ( F ` [_ A / x ]_ x ) = ( F ` A ) )
4 1 3 eqtrd 
 |-  ( A e. _V -> [_ A / x ]_ ( F ` x ) = ( F ` A ) )
5 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F ` x ) = (/) )
6 fvprc 
 |-  ( -. A e. _V -> ( F ` A ) = (/) )
7 5 6 eqtr4d 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F ` x ) = ( F ` A ) )
8 4 7 pm2.61i 
 |-  [_ A / x ]_ ( F ` x ) = ( F ` A )