Definition df-ima 4622

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 4621) and range (df-rn 4620). For an alternate definition, see dfima2 4953. (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 4612	. 2 class ( A " B )
4	1, 2	cres 4611	. . 3 class ( A |` B )
5	4	crn 4610	. 2 class ran ( A |` B )
6	3, 5	wceq 1348	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4922  resima2  4923  imaeq1  4946  imaeq2  4947  dfima2  4953  nfima  4959  rnresi  4966  resiima  4967  ima0  4968  imadisj  4971  imass1  4984  imass2  4985  ndmima  4986  imaundi  5021  imaundir  5022  inimass  5025  rninxp  5052  imainrect  5054  xpima1  5055  xpima2m  5056  dfrn4  5069  imacnvcnv  5073  imadmres  5101  mptpreima  5102  rnco2  5116  funcnvres  5269  funimacnv  5272  funimaexg  5280  fnima  5314  fores  5427  f1ores  5455  f1orescnv  5456  foimacnv  5458  resdif  5462  funfvima  5724  resfunexgALT  6084  smores2  6270  sbthlemi4  6933  sbthlemi6  6935  sbthlemi8  6937  djuin  7037  djuun  7040  casedm  7059  eninl  7070  eninr  7071  djudm  7078  tgrest  12922  cnconst2  12986  hmeores  13068