Step 
Hyp 
Ref 
Expression 
1 

dffn5 
 ( F Fn A <> F = ( x e. A > ( F ` x ) ) ) 
2 

dffn5 
 ( G Fn A <> G = ( x e. A > ( G ` x ) ) ) 
3 

eqeq12 
 ( ( F = ( x e. A > ( F ` x ) ) /\ G = ( x e. A > ( G ` x ) ) ) > ( F = G <> ( x e. A > ( F ` x ) ) = ( x e. A > ( G ` x ) ) ) ) 
4 
1 2 3

syl2anb 
 ( ( F Fn A /\ G Fn A ) > ( F = G <> ( x e. A > ( F ` x ) ) = ( x e. A > ( G ` x ) ) ) ) 
5 

fvex 
 ( F ` x ) e. _V 
6 
5

rgenw 
 A. x e. A ( F ` x ) e. _V 
7 

mpteqb 
 ( A. x e. A ( F ` x ) e. _V > ( ( x e. A > ( F ` x ) ) = ( x e. A > ( G ` x ) ) <> A. x e. A ( F ` x ) = ( G ` x ) ) ) 
8 
6 7

axmp 
 ( ( x e. A > ( F ` x ) ) = ( x e. A > ( G ` x ) ) <> A. x e. A ( F ` x ) = ( G ` x ) ) 
9 
4 8

syl6bb 
 ( ( F Fn A /\ G Fn A ) > ( F = G <> A. x e. A ( F ` x ) = ( G ` x ) ) ) 