let x be set ; :: thesis: x .--> x = id {x}
for y, z being set holds
( [y,z] in x .--> x iff ( y in {x} & y = z ) )

proof

let y, z be set ; :: thesis: ( [y,z] in x .--> x iff ( y in {x} & y = z ) )
J: x .--> x = {[x,x]} by ZFMISC_1:35;
thus ( [y,z] in x .--> x implies ( y in {x} & y = z ) ) :: thesis: ( y in {x} & y = z implies [y,z] in x .--> x )

proof

assume [y,z] in x .--> x ; :: thesis: ( y in {x} & y = z )
then [y,z] = [x,x] by J, TARSKI:def 1;
then ( y = x & z = x ) by ZFMISC_1:33;
hence ( y in {x} & y = z ) by TARSKI:def 1; :: thesis: verum

end;

assume y in {x} ; :: thesis: ( not y = z or [y,z] in x .--> x )
then y = x by TARSKI:def 1;
hence ( not y = z or [y,z] in x .--> x ) by J, TARSKI:def 1; :: thesis: verum

end;

hence x .--> x = id {x} by RELAT_1:def 10; :: thesis: verum