Definition df-ima 4672

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 4671) and range (df-rn 4670). For an alternate definition, see dfima2 5007. (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 4662	. 2 class ( A " B )
4	1, 2	cres 4661	. . 3 class ( A |` B )
5	4	crn 4660	. 2 class ran ( A |` B )
6	3, 5	wceq 1364	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4975  resima2  4976  imaeq1  5000  imaeq2  5001  dfima2  5007  nfima  5013  mptima  5017  rnresi  5022  resiima  5023  ima0  5024  imadisj  5027  imass1  5040  imass2  5041  ndmima  5042  imaundi  5078  imaundir  5079  inimass  5082  rninxp  5109  imainrect  5111  xpima1  5112  xpima2m  5113  dfrn4  5126  imacnvcnv  5130  imadmres  5158  mptpreima  5159  rnco2  5173  funcnvres  5327  funimacnv  5330  funimaexg  5338  fnima  5372  fores  5486  f1ores  5515  f1orescnv  5516  foimacnv  5518  resdif  5522  funfvima  5790  resfunexgALT  6160  smores2  6347  sbthlemi4  7019  sbthlemi6  7021  sbthlemi8  7023  djuin  7123  djuun  7126  casedm  7145  eninl  7156  eninr  7157  djudm  7164  ghmima  13335  conjsubg  13347  rnrhmsubrg  13748  tgrest  14337  cnconst2  14401  hmeores  14483