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 ↾ 𝐴 ) = ( I ↾ 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvin | ⊢ ◡ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( ◡ I ∩ ◡ ( 𝐴 × 𝐴 ) ) | |
| 2 | cnvi | ⊢ ◡ I = I | |
| 3 | cnvxp | ⊢ ◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 ) | |
| 4 | 2 3 | ineq12i | ⊢ ( ◡ I ∩ ◡ ( 𝐴 × 𝐴 ) ) = ( I ∩ ( 𝐴 × 𝐴 ) ) |
| 5 | 1 4 | eqtri | ⊢ ◡ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ∩ ( 𝐴 × 𝐴 ) ) |
| 6 | idinxpresid | ⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 ) | |
| 7 | 6 | cnveqi | ⊢ ◡ ( I ∩ ( 𝐴 × 𝐴 ) ) = ◡ ( I ↾ 𝐴 ) |
| 8 | 5 7 6 | 3eqtr3i | ⊢ ◡ ( I ↾ 𝐴 ) = ( I ↾ 𝐴 ) |