Definition df-ima 4676

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 4675) and range (df-rn 4674). For an alternate definition, see dfima2 5011. (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 4666	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4665	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4664	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1364	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4979  resima2  4980  imaeq1  5004  imaeq2  5005  dfima2  5011  nfima  5017  mptima  5021  rnresi  5026  resiima  5027  ima0  5028  imadisj  5031  imass1  5044  imass2  5045  ndmima  5046  imaundi  5082  imaundir  5083  inimass  5086  rninxp  5113  imainrect  5115  xpima1  5116  xpima2m  5117  dfrn4  5130  imacnvcnv  5134  imadmres  5162  mptpreima  5163  rnco2  5177  funcnvres  5331  funimacnv  5334  funimaexg  5342  fnima  5376  fores  5490  f1ores  5519  f1orescnv  5520  foimacnv  5522  resdif  5526  funfvima  5794  resfunexgALT  6165  smores2  6352  sbthlemi4  7026  sbthlemi6  7028  sbthlemi8  7030  djuin  7130  djuun  7133  casedm  7152  eninl  7163  eninr  7164  djudm  7171  ghmima  13395  conjsubg  13407  rnrhmsubrg  13808  tgrest  14405  cnconst2  14469  hmeores  14551  fsumdvdsmul  15227