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

Metamath Proof Explorer

Theorem eqbrrdiv

Description: Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 eqbrrdiv.1 ⊢ Rel ⁡ A
2 eqbrrdiv.2 ⊢ Rel ⁡ B
3 eqbrrdiv.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 1 2 6 eqrelrdv ⊢ φ → A = B