let R1, R2 be Equivalence_Relation of Prop Q; :: thesis: ( ( for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) ) & ( for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ) implies R1 = R2 )
assume A5: ( ( for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) ) & ( for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ) ) ; :: thesis: R1 = R2

A6: now

let p, q be Element of Prop Q; :: thesis: ( [p,q] in R1 iff [p,q] in R2 )
( ( [p,q] in R1 implies p <==> q ) & ( p <==> q implies [p,q] in R1 ) & ( [p,q] in R2 implies p <==> q ) & ( p <==> q implies [p,q] in R2 ) ) by A5;
hence ( [p,q] in R1 iff [p,q] in R2 ) ; :: thesis: verum

end;

for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )

proof

let x, y be set ; :: thesis: ( [x,y] in R1 iff [x,y] in R2 )
thus ( [x,y] in R1 implies [x,y] in R2 ) :: thesis: ( [x,y] in R2 implies [x,y] in R1 )

proof

assume A7: [x,y] in R1 ; :: thesis: [x,y] in R2
then ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:106;
hence [x,y] in R2 by A6, A7; :: thesis: verum

end;

assume A8: [x,y] in R2 ; :: thesis: [x,y] in R1
then ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:106;
hence [x,y] in R1 by A6, A8; :: thesis: verum

end;

hence R1 = R2 by RELAT_1:def 2; :: thesis: verum