Metamath Proof Explorer


Theorem cossssid5

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion cossssid5 R I x ran R y ran R x = y x R -1 y R -1 =

Proof

Step Hyp Ref Expression
1 cossssid4 R I u * x u R x
2 ineccnvmo2 x ran R y ran R x = y x R -1 y R -1 = u * x u R x
3 1 2 bitr4i R I x ran R y ran R x = y x R -1 y R -1 =