Description: A restricted identity relation is equal to its converse. (Contributed by FL, 4-Mar-2007) Remove dependency on ax-12 and shorten. (Revised by BJ, 1-Nov-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | cnvresid | |- `' ( _I |` A ) = ( _I |` A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvin | |- `' ( _I i^i ( A X. A ) ) = ( `' _I i^i `' ( A X. A ) ) |
|
| 2 | cnvi | |- `' _I = _I |
|
| 3 | cnvxp | |- `' ( A X. A ) = ( A X. A ) |
|
| 4 | 2 3 | ineq12i | |- ( `' _I i^i `' ( A X. A ) ) = ( _I i^i ( A X. A ) ) |
| 5 | 1 4 | eqtri | |- `' ( _I i^i ( A X. A ) ) = ( _I i^i ( A X. A ) ) |
| 6 | idinxpresid | |- ( _I i^i ( A X. A ) ) = ( _I |` A ) |
|
| 7 | 6 | cnveqi | |- `' ( _I i^i ( A X. A ) ) = `' ( _I |` A ) |
| 8 | 5 7 6 | 3eqtr3i | |- `' ( _I |` A ) = ( _I |` A ) |