This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -1 = I

Proof

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