Definition df-ima 4731

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 4730) and range (df-rn 4729). For an alternate definition, see dfima2 5069. (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 4721	. 2 class ( A " B )
4	1, 2	cres 4720	. . 3 class ( A |` B )
5	4	crn 4719	. 2 class ran ( A |` B )
6	3, 5	wceq 1395	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  5037  resima2  5038  imaeq1  5062  imaeq2  5063  dfima2  5069  nfima  5075  mptima  5079  rnresi  5084  resiima  5085  ima0  5086  imadisj  5089  imass1  5102  imass2  5103  ndmima  5104  imaundi  5140  imaundir  5141  inimass  5144  rninxp  5171  imainrect  5173  xpima1  5174  xpima2m  5175  dfrn4  5188  imacnvcnv  5192  imadmres  5220  mptpreima  5221  rnco2  5235  funcnvres  5393  funimacnv  5396  funimaexg  5404  fnima  5441  fores  5557  f1ores  5586  f1orescnv  5587  foimacnv  5589  resdif  5593  funfvima  5870  resfunexgALT  6251  smores2  6438  sbthlemi4  7123  sbthlemi6  7125  sbthlemi8  7127  djuin  7227  djuun  7230  casedm  7249  eninl  7260  eninr  7261  djudm  7268  ghmima  13797  conjsubg  13809  rnrhmsubrg  14210  tgrest  14837  cnconst2  14901  hmeores  14983  fsumdvdsmul  15659