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