Definition df-ima 4336

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 4335) and range (df-rn 4334). For an alternate definition, see dfima2 4648. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-ima	⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cima 4326	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4325	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4324	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1243	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4621  resima2  4622  imaeq1  4641  imaeq2  4642  dfima2  4648  nfima  4654  rnresi  4660  resiima  4661  ima0  4662  imadisj  4665  imass1  4678  imass2  4679  ndmima  4680  imaundi  4714  imaundir  4715  inimass  4718  rninxp  4742  imainrect  4744  xpima1  4745  xpima2m  4746  dfrn4  4759  imacnvcnv  4763  imadmres  4791  mptpreima  4792  rnco2  4806  funcnvres  4950  funimacnv  4953  funimaexg  4961  fnima  4995  fores  5093  f1ores  5119  f1orescnv  5120  foimacnv  5122  resdif  5126  funfvima  5368  resfunexgALT  5715  smores2  5887