Definition df-ima 4624

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 4623) and range (df-rn 4622). For an alternate definition, see dfima2 4955. (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 4614	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4613	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4612	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1348	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4924  resima2  4925  imaeq1  4948  imaeq2  4949  dfima2  4955  nfima  4961  rnresi  4968  resiima  4969  ima0  4970  imadisj  4973  imass1  4986  imass2  4987  ndmima  4988  imaundi  5023  imaundir  5024  inimass  5027  rninxp  5054  imainrect  5056  xpima1  5057  xpima2m  5058  dfrn4  5071  imacnvcnv  5075  imadmres  5103  mptpreima  5104  rnco2  5118  funcnvres  5271  funimacnv  5274  funimaexg  5282  fnima  5316  fores  5429  f1ores  5457  f1orescnv  5458  foimacnv  5460  resdif  5464  funfvima  5727  resfunexgALT  6087  smores2  6273  sbthlemi4  6937  sbthlemi6  6939  sbthlemi8  6941  djuin  7041  djuun  7044  casedm  7063  eninl  7074  eninr  7075  djudm  7082  tgrest  12963  cnconst2  13027  hmeores  13109