Theorem eqbrriv

Description: Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006)

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

Proof

Step	Hyp	Ref	Expression
1		eqbrriv.1	|- Rel A
2		eqbrriv.2	|- Rel B
3		eqbrriv.3	|- ( x A y <-> x B y )
4		df-br	|- ( x A y <-> <. x , y >. e. A )
5		df-br	|- ( x B y <-> <. x , y >. e. B )
6	3 4 5	3bitr3i	|- ( <. x , y >. e. A <-> <. x , y >. e. B )
7	1 2 6	eqrelriiv	|- A = B