This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )