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 ⊢ φ → A ⊆ C × D
eqbrrdva.2 ⊢ φ → B ⊆ C × D
eqbrrdva.3 ⊢ φ ∧ x ∈ C ∧ y ∈ D → x A y ↔ x B y
Assertion eqbrrdva ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 eqbrrdva.1 ⊢ φ → A ⊆ C × D
2 eqbrrdva.2 ⊢ φ → B ⊆ C × D
3 eqbrrdva.3 ⊢ φ ∧ x ∈ C ∧ y ∈ D → x A y ↔ x B y
4 xpss ⊢ C × D ⊆ V × V
5 1 4 sstrdi ⊢ φ → A ⊆ V × V
6 df-rel ⊢ Rel ⁡ A ↔ A ⊆ V × V
7 5 6 sylibr ⊢ φ → Rel ⁡ A
8 2 4 sstrdi ⊢ φ → B ⊆ V × V
9 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
10 8 9 sylibr ⊢ φ → Rel ⁡ B
11 1 ssbrd ⊢ φ → x A y → x C × D y
12 brxp ⊢ x C × D y ↔ x ∈ C ∧ y ∈ D
13 11 12 imbitrdi ⊢ φ → x A y → x ∈ C ∧ y ∈ D
14 2 ssbrd ⊢ φ → x B y → x C × D y
15 14 12 imbitrdi ⊢ φ → x B y → x ∈ C ∧ y ∈ D
16 3 3expib ⊢ φ → x ∈ C ∧ y ∈ D → x A y ↔ x B y
17 13 15 16 pm5.21ndd ⊢ φ → x A y ↔ x B y
18 7 10 17 eqbrrdv ⊢ φ → A = B