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} ) )

for v being object holds

( v in {x} iff ( v in dom {[x,y]} & {[x,y]} . v in {y} ) )

proof

hence
{[x,y]} " {y} = {x}
by FUNCT_1:def 7; :: thesis: verum
let v be object ; :: thesis: ( v in {x} iff ( v in dom {[x,y]} & {[x,y]} . v in {y} ) )

hence v in {x} by RELAT_1:9; :: thesis: verum

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

assume
( v in dom {[x,y]} & {[x,y]} . v in {y} )
; :: thesis: 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;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

hence v in {x} by RELAT_1:9; :: thesis: verum