Definition df-ima 4490

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 4489) and range (df-rn 4488). For an alternate definition, see dfima2 4819. (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 4480	. 2 class ( A " B )
4	1, 2	cres 4479	. . 3 class ( A |` B )
5	4	crn 4478	. 2 class ran ( A |` B )
6	3, 5	wceq 1299	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4788  resima2  4789  imaeq1  4812  imaeq2  4813  dfima2  4819  nfima  4825  rnresi  4832  resiima  4833  ima0  4834  imadisj  4837  imass1  4850  imass2  4851  ndmima  4852  imaundi  4887  imaundir  4888  inimass  4891  rninxp  4918  imainrect  4920  xpima1  4921  xpima2m  4922  dfrn4  4935  imacnvcnv  4939  imadmres  4967  mptpreima  4968  rnco2  4982  funcnvres  5132  funimacnv  5135  funimaexg  5143  fnima  5177  fores  5290  f1ores  5316  f1orescnv  5317  foimacnv  5319  resdif  5323  funfvima  5581  resfunexgALT  5939  smores2  6121  sbthlemi4  6776  sbthlemi6  6778  sbthlemi8  6780  djuin  6864  djuun  6867  casedm  6886  eninl  6897  eninr  6898  djudm  6905  tgrest  12120  cnconst2  12183