Metamath Proof Explorer


Theorem eqvrelcoss4

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019) (Revised by Peter Mazsa, 30-Sep-2021)

Ref Expression
Assertion eqvrelcoss4 EqvRelRxzxRzRxR-1zR-1

Proof

Step Hyp Ref Expression
1 eqvrelcoss3 EqvRelRxyzxRyyRzxRz
2 trcoss2 xyzxRyyRzxRzxzxRzRxR-1zR-1
3 1 2 bitri EqvRelRxzxRzRxR-1zR-1