Metamath Proof Explorer


Theorem brcoss2

Description: Alternate form of the A and B are cosets by R binary relation. (Contributed by Peter Mazsa, 26-Mar-2019)

Ref Expression
Assertion brcoss2 A V B W A R B u A u R B u R

Proof

Step Hyp Ref Expression
1 brcoss A V B W A R B u u R A u R B
2 exan3 A V B W u A u R B u R u u R A u R B
3 1 2 bitr4d A V B W A R B u A u R B u R