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 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐶 × 𝐷 ) )
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 ⊢ ( 𝜑 → 𝐴 = 𝐵 )