Theorem eqrelrdv

Description: Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010)

	Ref	Expression
Hypotheses	eqrelrdv.1	|- Rel A
	eqrelrdv.2	|- Rel B
	eqrelrdv.3	|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
Assertion	eqrelrdv	|- ( ph -> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqrelrdv.1	|- Rel A
2		eqrelrdv.2	|- Rel B
3		eqrelrdv.3	|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
4	3	alrimivv	|- ( ph -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
5		eqrel	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
6	1 2 5	mp2an	|- ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
7	4 6	sylibr	|- ( ph -> A = B )