Theorem eqbrrdv2

Description: Other version of eqbrrdiv . (Contributed by Rodolfo Medina, 30-Sep-2010)

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

Proof

Step	Hyp	Ref	Expression
1		eqbrrdv2.1	|- ( ( ( Rel A /\ Rel B ) /\ ph ) -> ( x A y <-> x B y ) )
2		df-br	|- ( x A y <-> <. x , y >. e. A )
3		df-br	|- ( x B y <-> <. x , y >. e. B )
4	1 2 3	3bitr3g	|- ( ( ( Rel A /\ Rel B ) /\ ph ) -> ( <. x , y >. e. A <-> <. x , y >. e. B ) )
5	4	eqrelrdv2	|- ( ( ( Rel A /\ Rel B ) /\ ( ( Rel A /\ Rel B ) /\ ph ) ) -> A = B )
6	5	anabss5	|- ( ( ( Rel A /\ Rel B ) /\ ph ) -> A = B )