Theorem eqbrrdiv

Description: Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		eqbrrdiv.1	|- Rel A
2		eqbrrdiv.2	|- Rel B
3		eqbrrdiv.3	|- ( ph -> ( 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	3bitr3g	|- ( ph -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
7	1 2 6	eqrelrdv	|- ( ph -> A = B )