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