Definition df-ima 4687

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

This definition is referenced by:  resima  4991  resima2  4992  imaeq1  5016  imaeq2  5017  dfima2  5023  nfima  5029  mptima  5033  rnresi  5038  resiima  5039  ima0  5040  imadisj  5043  imass1  5056  imass2  5057  ndmima  5058  imaundi  5094  imaundir  5095  inimass  5098  rninxp  5125  imainrect  5127  xpima1  5128  xpima2m  5129  dfrn4  5142  imacnvcnv  5146  imadmres  5174  mptpreima  5175  rnco2  5189  funcnvres  5346  funimacnv  5349  funimaexg  5357  fnima  5393  fores  5507  f1ores  5536  f1orescnv  5537  foimacnv  5539  resdif  5543  funfvima  5815  resfunexgALT  6192  smores2  6379  sbthlemi4  7061  sbthlemi6  7063  sbthlemi8  7065  djuin  7165  djuun  7168  casedm  7187  eninl  7198  eninr  7199  djudm  7206  ghmima  13543  conjsubg  13555  rnrhmsubrg  13956  tgrest  14583  cnconst2  14647  hmeores  14729  fsumdvdsmul  15405