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

Metamath Proof Explorer

Theorem brabsb2

Description: A closed form of brabsb . (Contributed by Rodolfo Medina, 13-Oct-2010)

Ref Expression
Assertion brabsb2 ⊢ R = x y | φ → z R w ↔ z x w y φ

Proof

Step Hyp Ref Expression
1 breq ⊢ R = x y | φ → z R w ↔ z x y | φ w
2 df-br ⊢ z x y | φ w ↔ z w ∈ x y | φ
3 1 2 bitrdi ⊢ R = x y | φ → z R w ↔ z w ∈ x y | φ
4 vopelopabsb ⊢ z w ∈ x y | φ ↔ z x w y φ
5 3 4 bitrdi ⊢ R = x y | φ → z R w ↔ z x w y φ