Definition df-ima 4738

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 4737) and range (df-rn 4736). For an alternate definition, see dfima2 5078. (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 4728	. 2 class ( A " B )
4	1, 2	cres 4727	. . 3 class ( A |` B )
5	4	crn 4726	. 2 class ran ( A |` B )
6	3, 5	wceq 1397	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  5046  resima2  5047  imaeq1  5071  imaeq2  5072  dfima2  5078  nfima  5084  mptima  5088  rnresi  5093  resiima  5094  ima0  5095  imadisj  5098  imass1  5111  imass2  5112  ndmima  5113  imaundi  5149  imaundir  5150  inimass  5153  rninxp  5180  imainrect  5182  xpima1  5183  xpima2m  5184  dfrn4  5197  imacnvcnv  5201  imadmres  5229  mptpreima  5230  rnco2  5244  funcnvres  5403  funimacnv  5406  funimaexg  5414  fnima  5451  fores  5569  f1ores  5598  f1orescnv  5599  foimacnv  5601  resdif  5605  funfvima  5886  resfunexgALT  6270  smores2  6460  sbthlemi4  7159  sbthlemi6  7161  sbthlemi8  7163  djuin  7263  djuun  7266  casedm  7285  eninl  7296  eninr  7297  djudm  7304  ghmima  13870  conjsubg  13882  rnrhmsubrg  14285  tgrest  14912  cnconst2  14976  hmeores  15058  fsumdvdsmul  15734