Definition df-ima 4696

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

This definition is referenced by:  resima  5001  resima2  5002  imaeq1  5026  imaeq2  5027  dfima2  5033  nfima  5039  mptima  5043  rnresi  5048  resiima  5049  ima0  5050  imadisj  5053  imass1  5066  imass2  5067  ndmima  5068  imaundi  5104  imaundir  5105  inimass  5108  rninxp  5135  imainrect  5137  xpima1  5138  xpima2m  5139  dfrn4  5152  imacnvcnv  5156  imadmres  5184  mptpreima  5185  rnco2  5199  funcnvres  5356  funimacnv  5359  funimaexg  5367  fnima  5404  fores  5520  f1ores  5549  f1orescnv  5550  foimacnv  5552  resdif  5556  funfvima  5829  resfunexgALT  6206  smores2  6393  sbthlemi4  7077  sbthlemi6  7079  sbthlemi8  7081  djuin  7181  djuun  7184  casedm  7203  eninl  7214  eninr  7215  djudm  7222  ghmima  13676  conjsubg  13688  rnrhmsubrg  14089  tgrest  14716  cnconst2  14780  hmeores  14862  fsumdvdsmul  15538