Metamath Proof Explorer


Theorem cossssid3

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

Ref Expression
Assertion cossssid3 R I u x y u R x u R y x = y

Proof

Step Hyp Ref Expression
1 cossssid2 R I x y u u R x u R y x = y
2 19.23v u u R x u R y x = y u u R x u R y x = y
3 2 albii y u u R x u R y x = y y u u R x u R y x = y
4 alcom y u u R x u R y x = y u y u R x u R y x = y
5 3 4 bitr3i y u u R x u R y x = y u y u R x u R y x = y
6 5 albii x y u u R x u R y x = y x u y u R x u R y x = y
7 alcom x u y u R x u R y x = y u x y u R x u R y x = y
8 1 6 7 3bitri R I u x y u R x u R y x = y