Metamath Proof Explorer


Theorem cosselcnvrefrels3

Description: Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 30-Aug-2021)

Ref Expression
Assertion cosselcnvrefrels3 R CnvRefRels u x y u R x u R y x = y R Rels

Proof

Step Hyp Ref Expression
1 cosselcnvrefrels2 R CnvRefRels R I R Rels
2 cossssid3 R I u x y u R x u R y x = y
3 2 anbi1i R I R Rels u x y u R x u R y x = y R Rels
4 1 3 bitri R CnvRefRels u x y u R x u R y x = y R Rels