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

Metamath Proof Explorer

Theorem eqbrrdva

Description: Deduction from extensionality principle for relations, given an equivalence only on the relation domain and range. (Contributed by Thierry Arnoux, 28-Nov-2017)

Ref Expression
Hypotheses eqbrrdva.1 
|- ( ph -> A C_ ( C X. D ) )
eqbrrdva.2 
|- ( ph -> B C_ ( C X. D ) )
eqbrrdva.3 
|- ( ( ph /\ x e. C /\ y e. D ) -> ( x A y <-> x B y ) )
Assertion eqbrrdva 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 eqbrrdva.1 
 |-  ( ph -> A C_ ( C X. D ) )
2 eqbrrdva.2 
 |-  ( ph -> B C_ ( C X. D ) )
3 eqbrrdva.3 
 |-  ( ( ph /\ x e. C /\ y e. D ) -> ( x A y <-> x B y ) )
4 xpss 
 |-  ( C X. D ) C_ ( _V X. _V )
5 1 4 sstrdi 
 |-  ( ph -> A C_ ( _V X. _V ) )
6 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
7 5 6 sylibr 
 |-  ( ph -> Rel A )
8 2 4 sstrdi 
 |-  ( ph -> B C_ ( _V X. _V ) )
9 df-rel 
 |-  ( Rel B <-> B C_ ( _V X. _V ) )
10 8 9 sylibr 
 |-  ( ph -> Rel B )
11 1 ssbrd 
 |-  ( ph -> ( x A y -> x ( C X. D ) y ) )
12 brxp 
 |-  ( x ( C X. D ) y <-> ( x e. C /\ y e. D ) )
13 11 12 imbitrdi 
 |-  ( ph -> ( x A y -> ( x e. C /\ y e. D ) ) )
14 2 ssbrd 
 |-  ( ph -> ( x B y -> x ( C X. D ) y ) )
15 14 12 imbitrdi 
 |-  ( ph -> ( x B y -> ( x e. C /\ y e. D ) ) )
16 3 3expib 
 |-  ( ph -> ( ( x e. C /\ y e. D ) -> ( x A y <-> x B y ) ) )
17 13 15 16 pm5.21ndd 
 |-  ( ph -> ( x A y <-> x B y ) )
18 7 10 17 eqbrrdv 
 |-  ( ph -> A = B )