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 | |- ( A |` ( B i^i dom A ) ) = ( A |` B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmres | |- dom ( A |` B ) = ( B i^i dom A ) |
|
| 2 | 1 | reseq2i | |- ( ( A |` B ) |` dom ( A |` B ) ) = ( ( A |` B ) |` ( B i^i dom A ) ) |
| 3 | relres | |- Rel ( A |` B ) |
|
| 4 | resdm | |- ( Rel ( A |` B ) -> ( ( A |` B ) |` dom ( A |` B ) ) = ( A |` B ) ) |
|
| 5 | 3 4 | ax-mp | |- ( ( A |` B ) |` dom ( A |` B ) ) = ( A |` B ) |
| 6 | inss1 | |- ( B i^i dom A ) C_ B |
|
| 7 | 6 | resabs1i | |- ( ( A |` B ) |` ( B i^i dom A ) ) = ( A |` ( B i^i dom A ) ) |
| 8 | 2 5 7 | 3eqtr3ri | |- ( A |` ( B i^i dom A ) ) = ( A |` B ) |