Metamath Proof Explorer


Theorem br2coss

Description: Cosets by ,R binary relation. (Contributed by Peter Mazsa, 25-Aug-2019)

Ref Expression
Assertion br2coss A V B W A R B A R B R

Proof

Step Hyp Ref Expression
1 brcoss3 A V B W A R B A R -1 B R -1
2 cnvcosseq R -1 = R
3 2 eceq2i A R -1 = A R
4 2 eceq2i B R -1 = B R
5 3 4 ineq12i A R -1 B R -1 = A R B R
6 5 neeq1i A R -1 B R -1 A R B R
7 1 6 bitrdi A V B W A R B A R B R