Step 
Hyp 
Ref 
Expression 
1 

ofc1.1 
 ( ph > A e. V ) 
2 

ofc1.2 
 ( ph > B e. W ) 
3 

ofc1.3 
 ( ph > F Fn A ) 
4 

ofc1.4 
 ( ( ph /\ X e. A ) > ( F ` X ) = C ) 
5 

fnconstg 
 ( B e. W > ( A X. { B } ) Fn A ) 
6 
2 5

syl 
 ( ph > ( A X. { B } ) Fn A ) 
7 

inidm 
 ( A i^i A ) = A 
8 

fvconst2g 
 ( ( B e. W /\ X e. A ) > ( ( A X. { B } ) ` X ) = B ) 
9 
2 8

sylan 
 ( ( ph /\ X e. A ) > ( ( A X. { B } ) ` X ) = B ) 
10 
6 3 1 1 7 9 4

ofval 
 ( ( ph /\ X e. A ) > ( ( ( A X. { B } ) oF R F ) ` X ) = ( B R C ) ) 