Description: The identity relation is a right-unit for composition. Part of Theorem 3.7(i) of Monk1 p. 36. (Contributed by NM, 22-Apr-2004) Strengthen to biconditional form and shorten (Revised by BJ, 16-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-coi1 | |- ( Rel A <-> ( A o. _I ) = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-dfrel3 | |- ( Rel A <-> ( A |` _V ) = A ) |
|
| 2 | coi1res | |- ( A o. _I ) = ( A |` _V ) |
|
| 3 | 2 | eqeq1i | |- ( ( A o. _I ) = A <-> ( A |` _V ) = A ) |
| 4 | 1 3 | bitr4i | |- ( Rel A <-> ( A o. _I ) = A ) |