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\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cima	$$classA\left[B\right]$$
3	0 1	cres	$$class\left({A\upharpoonright }_B\right)$$
4	3	crn	$$class\mathrm{ran}\left({A\upharpoonright }_B\right)$$
5	2 4	wceq	$$wffA\left[B\right]=\mathrm{ran}\left({A\upharpoonright }_B\right)$$