Definition df-ima

Description: Define the image of a class (as restricted by another class). Definition 6.6(2) of TakeutiZaring p. 24. For example, ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F " B ) = { 6 } ( ex-ima ). Contrast with restriction ( df-res ) and range ( df-rn ). For an alternate definition, see dfima2 . (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	df-ima	|- ( A " B ) = ran ( A |` B )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cima	|- ( A " B )
3	0 1	cres	|- ( A |` B )
4	3	crn	|- ran ( A |` B )
5	2 4	wceq	|- ( A " B ) = ran ( A |` B )