Theorem imadmres

Description: The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007)

	Ref	Expression
Assertion	imadmres	|- ( A " dom ( A |` B ) ) = ( A " B )

Proof

Step	Hyp	Ref	Expression
1		resdmres	|- ( A |` dom ( A |` B ) ) = ( A |` B )
2	1	rneqi	|- ran ( A |` dom ( A |` B ) ) = ran ( A |` B )
3		df-ima	|- ( A " dom ( A |` B ) ) = ran ( A |` dom ( A |` B ) )
4		df-ima	|- ( A " B ) = ran ( A |` B )
5	2 3 4	3eqtr4i	|- ( A " dom ( A |` B ) ) = ( A " B )