theorem :: BVFUNC_1:17

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )