Definition df-ima 4301

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 4300) and range (df-rn 4299). For an alternate definition, see dfima2 4613. (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 4291	. 2 class (A “ B)
4	1, 2	cres 4290	. . 3 class (A ↾ B)
5	4	crn 4289	. 2 class ran (A ↾ B)
6	3, 5	wceq 1242	1 wff (A “ B) = ran (A ↾ B)

This definition is referenced by:  resima  4586  resima2  4587  imaeq1  4606  imaeq2  4607  dfima2  4613  nfima  4619  rnresi  4625  resiima  4626  ima0  4627  imadisj  4630  imass1  4643  imass2  4644  ndmima  4645  imaundi  4679  imaundir  4680  inimass  4683  rninxp  4707  imainrect  4709  xpima1  4710  xpima2m  4711  dfrn4  4724  imacnvcnv  4728  imadmres  4756  mptpreima  4757  rnco2  4771  funcnvres  4915  funimacnv  4918  funimaexg  4926  fnima  4960  fores  5058  f1ores  5084  f1orescnv  5085  foimacnv  5087  resdif  5091  funfvima  5333  resfunexgALT  5679  smores2  5850