Definition df-ima 4686

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 4685) and range (df-rn 4684). For an alternate definition, see dfima2 5021. (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 4676	. 2 class ( A " B )
4	1, 2	cres 4675	. . 3 class ( A |` B )
5	4	crn 4674	. 2 class ran ( A |` B )
6	3, 5	wceq 1372	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4989  resima2  4990  imaeq1  5014  imaeq2  5015  dfima2  5021  nfima  5027  mptima  5031  rnresi  5036  resiima  5037  ima0  5038  imadisj  5041  imass1  5054  imass2  5055  ndmima  5056  imaundi  5092  imaundir  5093  inimass  5096  rninxp  5123  imainrect  5125  xpima1  5126  xpima2m  5127  dfrn4  5140  imacnvcnv  5144  imadmres  5172  mptpreima  5173  rnco2  5187  funcnvres  5341  funimacnv  5344  funimaexg  5352  fnima  5388  fores  5502  f1ores  5531  f1orescnv  5532  foimacnv  5534  resdif  5538  funfvima  5806  resfunexgALT  6183  smores2  6370  sbthlemi4  7044  sbthlemi6  7046  sbthlemi8  7048  djuin  7148  djuun  7151  casedm  7170  eninl  7181  eninr  7182  djudm  7189  ghmima  13519  conjsubg  13531  rnrhmsubrg  13932  tgrest  14559  cnconst2  14623  hmeores  14705  fsumdvdsmul  15381