Definition df-ima 4787

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 4786) and range (df-rn 4785). For an alternate definition, see dfima2 5128. (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 4777	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4776	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4775	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1402	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is used by:  resima  5096  resima2  5097  imaeq1  5121  imaeq2  5122  dfima2  5128  nfima  5134  mptima  5138  rnresi  5144  resiima  5145  ima0  5146  imadisj  5149  imass1  5162  imass2  5163  ndmima  5164  imaundi  5200  imaundir  5201  inimass  5204  rninxp  5231  imainrect  5233  xpima1  5234  xpima2m  5235  dfrn4  5248  imacnvcnv  5252  imadmres  5280  mptpreima  5281  rnco2  5295  funcnvres  5454  funimacnv  5457  funimaexg  5465  fnima  5502  fores  5625  f1ores  5654  f1orescnv  5655  foimacnv  5657  resdif  5661  funfvima  5950  resfunexgALT  6337  smores2  6565  sbthlemi4  7277  sbthlemi6  7279  sbthlemi8  7281  djuin  7404  djuun  7407  casedm  7426  eninl  7437  eninr  7438  djudm  7445  hashf1lem1  11285  ghmima  14068  conjsubg  14080  rnrhmsubrg  14560  tgrest  15270  cnconst2  15334  hmeores  15416  fsumdvdsmul  16105