let x, y be object ; :: thesis: {[x,y]} " {y} = {x}
for v being object holds
( v in {x} iff ( v in dom {[x,y]} & {[x,y]} . v in {y} ) )

proof

let v be object ; :: thesis: ( v in {x} iff ( v in dom {[x,y]} & {[x,y]} . v in {y} ) )

hereby :: thesis: ( v in dom {[x,y]} & {[x,y]} . v in {y} implies v in {x} )

assume v in {x} ; :: thesis: ( v in dom {[x,y]} & {[x,y]} . v in {y} )
then L032: v = x by TARSKI:def 1;
L0325: [x,y] in {[x,y]} by TARSKI:def 1;
then L033: ( x in dom {[x,y]} & {[x,y]} . x = y ) by FUNCT_1:1;
thus v in dom {[x,y]} by L032, L0325, FUNCT_1:1; :: thesis: {[x,y]} . v in {y}
thus {[x,y]} . v in {y} by L033, TARSKI:def 1, L032; :: thesis: verum

end;

assume ( v in dom {[x,y]} & {[x,y]} . v in {y} ) ; :: thesis: v in {x}
hence v in {x} by RELAT_1:9; :: thesis: verum

end;

hence {[x,y]} " {y} = {x} by FUNCT_1:def 7; :: thesis: verum