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