Metamath Proof Explorer

Theorem csbima12

Description: Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006) (Revised by NM, 20-Aug-2018)

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

Proof

Step Hyp Ref Expression
1 csbeq1 
 |-  ( y = A -> [_ y / x ]_ ( F " B ) = [_ A / x ]_ ( F " B ) )
2 csbeq1 
 |-  ( y = A -> [_ y / x ]_ F = [_ A / x ]_ F )
3 csbeq1 
 |-  ( y = A -> [_ y / x ]_ B = [_ A / x ]_ B )
4 2 3 imaeq12d 
 |-  ( y = A -> ( [_ y / x ]_ F " [_ y / x ]_ B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
5 1 4 eqeq12d 
 |-  ( y = A -> ( [_ y / x ]_ ( F " B ) = ( [_ y / x ]_ F " [_ y / x ]_ B ) <-> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) ) )
6 vex 
 |-  y e. _V
7 nfcsb1v 
 |-  F/_ x [_ y / x ]_ F
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
9 7 8 nfima 
 |-  F/_ x ( [_ y / x ]_ F " [_ y / x ]_ B )
10 csbeq1a 
 |-  ( x = y -> F = [_ y / x ]_ F )
11 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
12 10 11 imaeq12d 
 |-  ( x = y -> ( F " B ) = ( [_ y / x ]_ F " [_ y / x ]_ B ) )
13 6 9 12 csbief 
 |-  [_ y / x ]_ ( F " B ) = ( [_ y / x ]_ F " [_ y / x ]_ B )
14 5 13 vtoclg 
 |-  ( A e. _V -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
15 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F " B ) = (/) )
16 csbprc 
 |-  ( -. A e. _V -> [_ A / x ]_ B = (/) )
17 16 imaeq2d 
 |-  ( -. A e. _V -> ( [_ A / x ]_ F " [_ A / x ]_ B ) = ( [_ A / x ]_ F " (/) ) )
18 ima0 
 |-  ( [_ A / x ]_ F " (/) ) = (/)
19 17 18 eqtr2di 
 |-  ( -. A e. _V -> (/) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
20 15 19 eqtrd 
 |-  ( -. A e. _V -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )
21 14 20 pm2.61i 
 |-  [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B )