:: deftheorem defines is_epsilon-isomorphism_of ZF_COLLA:def 2 :
for f being Function
for X, Y being set holds
( f is_epsilon-isomorphism_of X,Y iff ( dom f = X & rng f = Y & f is one-to-one & ( for x, y being object st x in X & y in X holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) ) ) ) );