let y, x, A, B be set ; :: thesis: for R being Subset of [:A,B:] holds
( y in Im (R ` ),x iff ( not [x,y] in R & x in A & y in B ) )
let R be Subset of [:A,B:]; :: thesis: ( y in Im (R ` ),x iff ( not [x,y] in R & x in A & y in B ) )
thus ( y in Im (R ` ),x implies ( not [x,y] in R & x in A & y in B ) ) :: thesis: ( not [x,y] in R & x in A & y in B implies y in Im (R ` ),x )

proof

assume y in Im (R ` ),x ; :: thesis: ( not [x,y] in R & x in A & y in B )
then ex a being set st
( [a,y] in R ` & a in {x} ) by RELAT_1:def 13;
then [x,y] in [:A,B:] \ R by TARSKI:def 1;
hence ( not [x,y] in R & x in A & y in B ) by XBOOLE_0:def 5, ZFMISC_1:106; :: thesis: verum

end;

assume that
A1: not [x,y] in R and
A2: x in A and
A3: y in B ; :: thesis: y in Im (R ` ),x
A4: x in {x} by TARSKI:def 1;
[x,y] in [:A,B:] by A2, A3, ZFMISC_1:106;
then [x,y] in [:A,B:] \ R by A1, XBOOLE_0:def 5;
hence y in Im (R ` ),x by A4, RELAT_1:def 13; :: thesis: verum