let x, X, Y be set ; :: thesis: ( x in X implies Im [:X,Y:],x = Y )
assume Z: x in X ; :: thesis: Im [:X,Y:],x = Y
thus Im [:X,Y:],x c= Y :: according to XBOOLE_0:def 10 :: thesis: Y c= Im [:X,Y:],x

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Im [:X,Y:],x or y in Y )
assume y in Im [:X,Y:],x ; :: thesis: y in Y
then consider z being set such that
W1: [z,y] in [:X,Y:] and
W2: z in {x} by Def13;
x = z by W2, TARSKI:def 1;
hence y in Y by W1, ZFMISC_1:106; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in Im [:X,Y:],x )
assume y in Y ; :: thesis: y in Im [:X,Y:],x
then A: [x,y] in [:X,Y:] by Z, ZFMISC_1:106;
x in {x} by TARSKI:def 1;
hence y in Im [:X,Y:],x by A, Def13; :: thesis: verum