Metamath Proof Explorer

Theorem csbfv12

Description: Move class substitution in and out of a function value. (Contributed by NM, 11-Nov-2005) (Revised by NM, 20-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 csbiota 
 |-  [_ A / x ]_ ( iota y B F y ) = ( iota y [. A / x ]. B F y )
2 sbcbr123 
 |-  ( [. A / x ]. B F y <-> [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ y )
3 csbconstg 
 |-  ( A e. _V -> [_ A / x ]_ y = y )
4 3 breq2d 
 |-  ( A e. _V -> ( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ y <-> [_ A / x ]_ B [_ A / x ]_ F y ) )
5 2 4 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. B F y <-> [_ A / x ]_ B [_ A / x ]_ F y ) )
6 5 iotabidv 
 |-  ( A e. _V -> ( iota y [. A / x ]. B F y ) = ( iota y [_ A / x ]_ B [_ A / x ]_ F y ) )
7 1 6 eqtrid 
 |-  ( A e. _V -> [_ A / x ]_ ( iota y B F y ) = ( iota y [_ A / x ]_ B [_ A / x ]_ F y ) )
8 df-fv 
 |-  ( F ` B ) = ( iota y B F y )
9 8 csbeq2i 
 |-  [_ A / x ]_ ( F ` B ) = [_ A / x ]_ ( iota y B F y )
10 df-fv 
 |-  ( [_ A / x ]_ F ` [_ A / x ]_ B ) = ( iota y [_ A / x ]_ B [_ A / x ]_ F y )
11 7 9 10 3eqtr4g 
 |-  ( A e. _V -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )
12 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F ` B ) = (/) )
13 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ F = (/) )
14 13 fveq1d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ F ` [_ A / x ]_ B ) = ( (/) ` [_ A / x ]_ B ) )
15 0fv 
 |-  ( (/) ` [_ A / x ]_ B ) = (/)
16 14 15 eqtr2di 
 |-  ( -. A e. _V -> (/) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )
17 12 16 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )
18 11 17 pm2.61i 
 |-  [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B )