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 )