Definition df-ima 4376

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 4375) and range (df-rn 4374). For an alternate definition, see dfima2 4690. (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 4366	. 2 class ( A " B )
4	1, 2	cres 4365	. . 3 class ( A |` B )
5	4	crn 4364	. 2 class ran ( A |` B )
6	3, 5	wceq 1284	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4661  resima2  4662  imaeq1  4683  imaeq2  4684  dfima2  4690  nfima  4696  rnresi  4702  resiima  4703  ima0  4704  imadisj  4707  imass1  4720  imass2  4721  ndmima  4722  imaundi  4756  imaundir  4757  inimass  4760  rninxp  4784  imainrect  4786  xpima1  4787  xpima2m  4788  dfrn4  4801  imacnvcnv  4805  imadmres  4833  mptpreima  4834  rnco2  4848  funcnvres  4992  funimacnv  4995  funimaexg  5003  fnima  5037  fores  5135  f1ores  5161  f1orescnv  5162  foimacnv  5164  resdif  5168  funfvima  5411  resfunexgALT  5757  smores2  5932