Let X, Y, f and V be given.

Assume Hfun: function_on f X Y.

rewrite the current goal using (preimage_of_setminus X f Y V) (from left to right).

rewrite the current goal using (preimage_of_whole X Y f Hfun) (from left to right).

Use reflexivity.

∎