Description: Cosets by the converse identity relation are the identity relation. (Contributed by Peter Mazsa, 27-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | cosscnvid | ⊢ ≀ ◡ I = I |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvi | ⊢ ◡ I = I | |
2 | 1 | cosseqi | ⊢ ≀ ◡ I = ≀ I |
3 | cossid | ⊢ ≀ I = I | |
4 | 2 3 | eqtri | ⊢ ≀ ◡ I = I |