Definition df-ima 4673

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 4672) and range (df-rn 4671). For an alternate definition, see dfima2 5008. (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 4663	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4662	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4661	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1364	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4976  resima2  4977  imaeq1  5001  imaeq2  5002  dfima2  5008  nfima  5014  mptima  5018  rnresi  5023  resiima  5024  ima0  5025  imadisj  5028  imass1  5041  imass2  5042  ndmima  5043  imaundi  5079  imaundir  5080  inimass  5083  rninxp  5110  imainrect  5112  xpima1  5113  xpima2m  5114  dfrn4  5127  imacnvcnv  5131  imadmres  5159  mptpreima  5160  rnco2  5174  funcnvres  5328  funimacnv  5331  funimaexg  5339  fnima  5373  fores  5487  f1ores  5516  f1orescnv  5517  foimacnv  5519  resdif  5523  funfvima  5791  resfunexgALT  6162  smores2  6349  sbthlemi4  7021  sbthlemi6  7023  sbthlemi8  7025  djuin  7125  djuun  7128  casedm  7147  eninl  7158  eninr  7159  djudm  7166  ghmima  13338  conjsubg  13350  rnrhmsubrg  13751  tgrest  14348  cnconst2  14412  hmeores  14494