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	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐶 × 𝐷 ) )
	eqbrrdva.2	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐶 × 𝐷 ) )
	eqbrrdva.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
Assertion	eqbrrdva	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqbrrdva.1	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐶 × 𝐷 ) )
2		eqbrrdva.2	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐶 × 𝐷 ) )
3		eqbrrdva.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
4		xpss	⊢ ( 𝐶 × 𝐷 ) ⊆ ( V × V )
5	1 4	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ( V × V ) )
6		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
7	5 6	sylibr	⊢ ( 𝜑 → Rel 𝐴 )
8	2 4	sstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( V × V ) )
9		df-rel	⊢ ( Rel 𝐵 ↔ 𝐵 ⊆ ( V × V ) )
10	8 9	sylibr	⊢ ( 𝜑 → Rel 𝐵 )
11	1	ssbrd	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 → 𝑥 ( 𝐶 × 𝐷 ) 𝑦 ) )
12		brxp	⊢ ( 𝑥 ( 𝐶 × 𝐷 ) 𝑦 ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) )
13	11 12	imbitrdi	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 → ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
14	2	ssbrd	⊢ ( 𝜑 → ( 𝑥 𝐵 𝑦 → 𝑥 ( 𝐶 × 𝐷 ) 𝑦 ) )
15	14 12	imbitrdi	⊢ ( 𝜑 → ( 𝑥 𝐵 𝑦 → ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
16	3	3expib	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) ) )
17	13 15 16	pm5.21ndd	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
18	7 10 17	eqbrrdv	⊢ ( 𝜑 → 𝐴 = 𝐵 )