let R1, R2 be Equivalence_Relation of (Prop Q); ( ( 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 that
A5:
for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q )
and
A6:
for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q )
; R1 = R2
A7:
for p, q being Element of Prop Q holds
( [p,q] in R1 iff [p,q] in R2 )
by A5, A6;
for x, y being object holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x,
y be
object ;
( [x,y] in R1 iff [x,y] in R2 )
thus
(
[x,y] in R1 implies
[x,y] in R2 )
( [x,y] in R2 implies [x,y] in R1 )
assume A9:
[x,y] in R2
;
[x,y] in R1
then
(
x is
Element of
Prop Q &
y is
Element of
Prop Q )
by ZFMISC_1:87;
hence
[x,y] in R1
by A7, A9;
verum
end;
hence
R1 = R2
by RELAT_1:def 2; verum