Definition df-ima 4414

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 } . Contrast with restriction (df-res 4413) and range (df-rn 4412). For an alternate definition, see dfima2 4731. (Contributed by NM, 2-Aug-1994.)

Assertion

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

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 4404	. 2 class ( A " B )
4	1, 2	cres 4403	. . 3 class ( A |` B )
5	4	crn 4402	. 2 class ran ( A |` B )
6	3, 5	wceq 1285	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4702  resima2  4703  imaeq1  4724  imaeq2  4725  dfima2  4731  nfima  4737  rnresi  4744  resiima  4745  ima0  4746  imadisj  4749  imass1  4762  imass2  4763  ndmima  4764  imaundi  4798  imaundir  4799  inimass  4802  rninxp  4828  imainrect  4830  xpima1  4831  xpima2m  4832  dfrn4  4845  imacnvcnv  4849  imadmres  4877  mptpreima  4878  rnco2  4892  funcnvres  5040  funimacnv  5043  funimaexg  5051  fnima  5085  fores  5190  f1ores  5216  f1orescnv  5217  foimacnv  5219  resdif  5223  funfvima  5466  resfunexgALT  5816  smores2  5991  djuun  6667  casedm  6684  djudm  6692