Description: When restricting a class, intersecting with the domain of the class has no effect. (Contributed by FL, 6-Oct-2008) Remove antecedent. (Revised by Eric Schmidt, 16-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | resindm | ⊢ ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmres | ⊢ dom ( 𝐴 ↾ 𝐵 ) = ( 𝐵 ∩ dom 𝐴 ) | |
| 2 | 1 | reseq2i | ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( ( 𝐴 ↾ 𝐵 ) ↾ ( 𝐵 ∩ dom 𝐴 ) ) |
| 3 | relres | ⊢ Rel ( 𝐴 ↾ 𝐵 ) | |
| 4 | resdm | ⊢ ( Rel ( 𝐴 ↾ 𝐵 ) → ( ( 𝐴 ↾ 𝐵 ) ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) ) | |
| 5 | 3 4 | ax-mp | ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ dom ( 𝐴 ↾ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 ) |
| 6 | inss1 | ⊢ ( 𝐵 ∩ dom 𝐴 ) ⊆ 𝐵 | |
| 7 | 6 | resabs1i | ⊢ ( ( 𝐴 ↾ 𝐵 ) ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) |
| 8 | 2 5 7 | 3eqtr3ri | ⊢ ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ 𝐵 ) |