let x be object ; :: thesis: x .--> x = id {x}
for y, z being object holds
( [y,z] in x .--> x iff ( y in {x} & y = z ) )
proof
let y, z be object ; :: thesis: ( [y,z] in x .--> x iff ( y in {x} & y = z ) )
A1: x .--> x = {[x,x]} by ZFMISC_1:29;
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 A2: [y,z] = [x,x] by A1, TARSKI:def 1;
then y = x by XTUPLE_0:1;
hence ( y in {x} & y = z ) by A2, TARSKI:def 1, XTUPLE_0: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 A1, TARSKI:def 1; :: thesis: verum
end;
hence x .--> x = id {x} by RELAT_1:def 10; :: thesis: verum