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

Metamath Proof Explorer

Theorem eqbrrdv

Description: Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 eqbrrdv.1 
 |-  ( ph -> Rel A )
2 eqbrrdv.2 
 |-  ( ph -> Rel B )
3 eqbrrdv.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 6 alrimivv 
 |-  ( ph -> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) )
8 eqrel 
 |-  ( ( Rel A /\ Rel B ) -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A = B <-> A. x A. y ( <. x , y >. e. A <-> <. x , y >. e. B ) ) )
10 7 9 mpbird 
 |-  ( ph -> A = B )