Theorem eqrelriv

Description: Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Hypothesis	eqrelriv.1	|- ( <. x , y >. e. A <-> <. x , y >. e. B )
Assertion	eqrelriv	|- ( ( Rel A /\ Rel B ) -> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqrelriv.1	|- ( <. x , y >. e. A <-> <. x , y >. e. B )
2	1	gen2	|- A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B )
3		eqrel	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
4	2 3	mpbiri	|- ( ( Rel A /\ Rel B ) -> A = B )