Metamath Proof Explorer


Theorem cosscnvid

Description: Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion cosscnvid I = I

Proof

Step Hyp Ref Expression
1 cnvi I = I
2 1 cosseqi I = ≀ I
3 cossid ≀ I = I
4 2 3 eqtri I = I