Definition df-ima 4709

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 4708) and range (df-rn 4707). For an alternate definition, see dfima2 5046. (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 4699	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4698	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4697	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1375	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5014  resima2  5015  imaeq1  5039  imaeq2  5040  dfima2  5046  nfima  5052  mptima  5056  rnresi  5061  resiima  5062  ima0  5063  imadisj  5066  imass1  5079  imass2  5080  ndmima  5081  imaundi  5117  imaundir  5118  inimass  5121  rninxp  5148  imainrect  5150  xpima1  5151  xpima2m  5152  dfrn4  5165  imacnvcnv  5169  imadmres  5197  mptpreima  5198  rnco2  5212  funcnvres  5370  funimacnv  5373  funimaexg  5381  fnima  5418  fores  5534  f1ores  5563  f1orescnv  5564  foimacnv  5566  resdif  5570  funfvima  5844  resfunexgALT  6223  smores2  6410  sbthlemi4  7095  sbthlemi6  7097  sbthlemi8  7099  djuin  7199  djuun  7202  casedm  7221  eninl  7232  eninr  7233  djudm  7240  ghmima  13768  conjsubg  13780  rnrhmsubrg  14181  tgrest  14808  cnconst2  14872  hmeores  14954  fsumdvdsmul  15630