Definition df-ima 4512

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 4511) and range (df-rn 4510). For an alternate definition, see dfima2 4841. (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 4502	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4501	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4500	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1314	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4810  resima2  4811  imaeq1  4834  imaeq2  4835  dfima2  4841  nfima  4847  rnresi  4854  resiima  4855  ima0  4856  imadisj  4859  imass1  4872  imass2  4873  ndmima  4874  imaundi  4909  imaundir  4910  inimass  4913  rninxp  4940  imainrect  4942  xpima1  4943  xpima2m  4944  dfrn4  4957  imacnvcnv  4961  imadmres  4989  mptpreima  4990  rnco2  5004  funcnvres  5154  funimacnv  5157  funimaexg  5165  fnima  5199  fores  5312  f1ores  5338  f1orescnv  5339  foimacnv  5341  resdif  5345  funfvima  5603  resfunexgALT  5962  smores2  6145  sbthlemi4  6800  sbthlemi6  6802  sbthlemi8  6804  djuin  6901  djuun  6904  casedm  6923  eninl  6934  eninr  6935  djudm  6942  tgrest  12181  cnconst2  12244