Definition df-ima 4785

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 4784) and range (df-rn 4783). For an alternate definition, see dfima2 5126. (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 4775	. 2 class ( A " B )
4	1, 2	cres 4774	. . 3 class ( A |` B )
5	4	crn 4773	. 2 class ran ( A |` B )
6	3, 5	wceq 1402	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  5094  resima2  5095  imaeq1  5119  imaeq2  5120  dfima2  5126  nfima  5132  mptima  5136  rnresi  5142  resiima  5143  ima0  5144  imadisj  5147  imass1  5160  imass2  5161  ndmima  5162  imaundi  5198  imaundir  5199  inimass  5202  rninxp  5229  imainrect  5231  xpima1  5232  xpima2m  5233  dfrn4  5246  imacnvcnv  5250  imadmres  5278  mptpreima  5279  rnco2  5293  funcnvres  5452  funimacnv  5455  funimaexg  5463  fnima  5500  fores  5623  f1ores  5652  f1orescnv  5653  foimacnv  5655  resdif  5659  funfvima  5943  resfunexgALT  6330  smores2  6558  sbthlemi4  7270  sbthlemi6  7272  sbthlemi8  7274  djuin  7397  djuun  7400  casedm  7419  eninl  7430  eninr  7431  djudm  7438  hashf1lem1  11266  ghmima  14048  conjsubg  14060  rnrhmsubrg  14536  tgrest  15196  cnconst2  15260  hmeores  15342  fsumdvdsmul  16022