Metamath Proof Explorer

Theorem resresdm

Description: A restriction by an arbitrary set is a restriction by its domain. (Contributed by AV, 16-Nov-2020)

Ref Expression
Assertion resresdm ⊢ F = E ↾ A → F = E ↾ dom ⁡ F

Proof

Step Hyp Ref Expression
1 id ⊢ F = E ↾ A → F = E ↾ A
2 dmeq ⊢ F = E ↾ A → dom ⁡ F = dom ⁡ E ↾ A
3 2 reseq2d ⊢ F = E ↾ A → E ↾ dom ⁡ F = E ↾ dom ⁡ E ↾ A
4 resdmres ⊢ E ↾ dom ⁡ E ↾ A = E ↾ A
5 3 4 eqtr2di ⊢ F = E ↾ A → E ↾ A = E ↾ dom ⁡ F
6 1 5 eqtrd ⊢ F = E ↾ A → F = E ↾ dom ⁡ F