Metamath Proof Explorer


Theorem cosscnvssid3

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, 28-Jul-2021)

Ref Expression
Assertion cosscnvssid3 R -1 I u v x u R x v R x u = v

Proof

Step Hyp Ref Expression
1 cossssid3 R -1 I x u v x R -1 u x R -1 v u = v
2 alrot3 x u v x R -1 u x R -1 v u = v u v x x R -1 u x R -1 v u = v
3 brcnvg x V u V x R -1 u u R x
4 3 el2v x R -1 u u R x
5 brcnvg x V v V x R -1 v v R x
6 5 el2v x R -1 v v R x
7 4 6 anbi12i x R -1 u x R -1 v u R x v R x
8 7 imbi1i x R -1 u x R -1 v u = v u R x v R x u = v
9 8 3albii u v x x R -1 u x R -1 v u = v u v x u R x v R x u = v
10 1 2 9 3bitri R -1 I u v x u R x v R x u = v