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∧φ→xAy↔xBy
Assertion eqbrrdv2 ⊢Rel⁡A∧Rel⁡B∧φ→A=B

Proof

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