Metamath Proof Explorer


Theorem cosscnvssid4

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

Ref Expression
Assertion cosscnvssid4 R -1 I x * u u R x

Proof

Step Hyp Ref Expression
1 cossssid4 R -1 I x * u x R -1 u
2 brcnvg x V u V x R -1 u u R x
3 2 el2v x R -1 u u R x
4 3 mobii * u x R -1 u * u u R x
5 4 albii x * u x R -1 u x * u u R x
6 1 5 bitri R -1 I x * u u R x