set u1 = the carrier of U1;
let X, Y be Congruence of U1; :: thesis: ( ( for a, b being Element of U1 holds
( [a,b] in X iff f . a = f . b ) ) & ( for a, b being Element of U1 holds
( [a,b] in Y iff f . a = f . b ) ) implies X = Y )
assume that
A23: for a, b being Element of U1 holds
( [a,b] in X iff f . a = f . b ) and
A24: for a, b being Element of U1 holds
( [a,b] in Y iff f . a = f . b ) ; :: thesis: X = Y
for x, y being object holds
( [x,y] in X iff [x,y] in Y )
proof
let x, y be object ; :: thesis: ( [x,y] in X iff [x,y] in Y )
thus ( [x,y] in X implies [x,y] in Y ) :: thesis: ( [x,y] in Y implies [x,y] in X )
proof
assume A25: [x,y] in X ; :: thesis: [x,y] in Y
then reconsider x1 = x, y1 = y as Element of the carrier of U1 by ZFMISC_1:87;
f . x1 = f . y1 by A23, A25;
hence [x,y] in Y by A24; :: thesis: verum
end;
assume A26: [x,y] in Y ; :: thesis: [x,y] in X
then reconsider x1 = x, y1 = y as Element of the carrier of U1 by ZFMISC_1:87;
f . x1 = f . y1 by A24, A26;
hence [x,y] in X by A23; :: thesis: verum
end;
hence X = Y by RELAT_1:def 2; :: thesis: verum