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

Metamath Proof Explorer

Theorem eqbrrdv2

Description: Other version of eqbrrdiv . (Contributed by Rodolfo Medina, 30-Sep-2010)

Ref Expression
Hypothesis eqbrrdv2.1 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → x A y ↔ x B y
Assertion eqbrrdv2 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B

Proof

Step Hyp Ref Expression
1 eqbrrdv2.1 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → x A y ↔ x B y
2 df-br ⊢ x A y ↔ x y ∈ A
3 df-br ⊢ x B y ↔ x y ∈ B
4 1 2 3 3bitr3g ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → x y ∈ A ↔ x y ∈ B
5 4 eqrelrdv2 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B
6 5 anabss5 ⊢ Rel ⁡ A ∧ Rel ⁡ B ∧ φ → A = B