Definition df-ima 4736

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 4735) and range (df-rn 4734). For an alternate definition, see dfima2 5076. (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 4726	. 2 class ( A " B )
4	1, 2	cres 4725	. . 3 class ( A |` B )
5	4	crn 4724	. 2 class ran ( A |` B )
6	3, 5	wceq 1395	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  5044  resima2  5045  imaeq1  5069  imaeq2  5070  dfima2  5076  nfima  5082  mptima  5086  rnresi  5091  resiima  5092  ima0  5093  imadisj  5096  imass1  5109  imass2  5110  ndmima  5111  imaundi  5147  imaundir  5148  inimass  5151  rninxp  5178  imainrect  5180  xpima1  5181  xpima2m  5182  dfrn4  5195  imacnvcnv  5199  imadmres  5227  mptpreima  5228  rnco2  5242  funcnvres  5400  funimacnv  5403  funimaexg  5411  fnima  5448  fores  5566  f1ores  5595  f1orescnv  5596  foimacnv  5598  resdif  5602  funfvima  5881  resfunexgALT  6265  smores2  6455  sbthlemi4  7150  sbthlemi6  7152  sbthlemi8  7154  djuin  7254  djuun  7257  casedm  7276  eninl  7287  eninr  7288  djudm  7295  ghmima  13842  conjsubg  13854  rnrhmsubrg  14256  tgrest  14883  cnconst2  14947  hmeores  15029  fsumdvdsmul  15705