Definition df-ima 4424

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 4423) and range (df-rn 4422). For an alternate definition, see dfima2 4743. (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 4414	. 2 class ( A " B )
4	1, 2	cres 4413	. . 3 class ( A |` B )
5	4	crn 4412	. 2 class ran ( A |` B )
6	3, 5	wceq 1287	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4712  resima2  4713  imaeq1  4736  imaeq2  4737  dfima2  4743  nfima  4749  rnresi  4756  resiima  4757  ima0  4758  imadisj  4761  imass1  4774  imass2  4775  ndmima  4776  imaundi  4810  imaundir  4811  inimass  4814  rninxp  4840  imainrect  4842  xpima1  4843  xpima2m  4844  dfrn4  4857  imacnvcnv  4861  imadmres  4889  mptpreima  4890  rnco2  4904  funcnvres  5052  funimacnv  5055  funimaexg  5063  fnima  5097  fores  5205  f1ores  5231  f1orescnv  5232  foimacnv  5234  resdif  5238  funfvima  5487  resfunexgALT  5838  smores2  6013  sbthlemi4  6613  sbthlemi6  6615  sbthlemi8  6617  djuun  6704  casedm  6721  djudm  6729