Step 
Hyp 
Ref 
Expression 
1 

imaco 
 ( ( F o. G ) " { X } ) = ( F " ( G " { X } ) ) 
2 

fnsnfv 
 ( ( G Fn A /\ X e. A ) > { ( G ` X ) } = ( G " { X } ) ) 
3 
2

imaeq2d 
 ( ( G Fn A /\ X e. A ) > ( F " { ( G ` X ) } ) = ( F " ( G " { X } ) ) ) 
4 
1 3

eqtr4id 
 ( ( G Fn A /\ X e. A ) > ( ( F o. G ) " { X } ) = ( F " { ( G ` X ) } ) ) 
5 
4

eleq2d 
 ( ( G Fn A /\ X e. A ) > ( x e. ( ( F o. G ) " { X } ) <> x e. ( F " { ( G ` X ) } ) ) ) 
6 
5

iotabidv 
 ( ( G Fn A /\ X e. A ) > ( iota x x e. ( ( F o. G ) " { X } ) ) = ( iota x x e. ( F " { ( G ` X ) } ) ) ) 
7 

dffv3 
 ( ( F o. G ) ` X ) = ( iota x x e. ( ( F o. G ) " { X } ) ) 
8 

dffv3 
 ( F ` ( G ` X ) ) = ( iota x x e. ( F " { ( G ` X ) } ) ) 
9 
6 7 8

3eqtr4g 
 ( ( G Fn A /\ X e. A ) > ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) ) 