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 ) )