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
A15: for a, b being Element of U1 holds
( [a,b] in X iff f . a = f . b ) and
A16: for a, b being Element of U1 holds
( [a,b] in Y iff f . a = f . b ) ; :: thesis: X = Y
set u1 = the carrier of U1;
for x, y being set holds
( [x,y] in X iff [x,y] in Y )

proof

let x, y be set ; :: 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 A17: [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:106;
f . x1 = f . y1 by A15, A17;
hence [x,y] in Y by A16; :: thesis: verum

end;

assume A18: [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:106;
f . x1 = f . y1 by A16, A18;
hence [x,y] in X by A15; :: thesis: verum

end;

hence X = Y by RELAT_1:def 2; :: thesis: verum