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

Metamath Proof Explorer

Theorem eqbrrdv

Description: Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses eqbrrdv.1 ⊢ φ → Rel ⁡ A
eqbrrdv.2 ⊢ φ → Rel ⁡ B
eqbrrdv.3 ⊢ φ → x A y ↔ x B y
Assertion eqbrrdv ⊢ φ → A = B

Proof

Step Hyp Ref Expression
1 eqbrrdv.1 ⊢ φ → Rel ⁡ A
2 eqbrrdv.2 ⊢ φ → Rel ⁡ B
3 eqbrrdv.3 ⊢ φ → x A y ↔ x B y
4 df-br ⊢ x A y ↔ x y ∈ A
5 df-br ⊢ x B y ↔ x y ∈ B
6 3 4 5 3bitr3g ⊢ φ → x y ∈ A ↔ x y ∈ B
7 6 alrimivv ⊢ φ → ∀ x ∀ y x y ∈ A ↔ x y ∈ B
8 eqrel ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B
9 1 2 8 syl2anc ⊢ φ → A = B ↔ ∀ x ∀ y x y ∈ A ↔ x y ∈ B
10 7 9 mpbird ⊢ φ → A = B