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 )