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	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → 𝐹 = ( 𝐸 ↾ dom 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → 𝐹 = ( 𝐸 ↾ 𝐴 ) )
2		dmeq	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → dom 𝐹 = dom ( 𝐸 ↾ 𝐴 ) )
3	2	reseq2d	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → ( 𝐸 ↾ dom 𝐹 ) = ( 𝐸 ↾ dom ( 𝐸 ↾ 𝐴 ) ) )
4		resdmres	⊢ ( 𝐸 ↾ dom ( 𝐸 ↾ 𝐴 ) ) = ( 𝐸 ↾ 𝐴 )
5	3 4	eqtr2di	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → ( 𝐸 ↾ 𝐴 ) = ( 𝐸 ↾ dom 𝐹 ) )
6	1 5	eqtrd	⊢ ( 𝐹 = ( 𝐸 ↾ 𝐴 ) → 𝐹 = ( 𝐸 ↾ dom 𝐹 ) )