Definition df-ima 4789

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

This definition is used by:  resima  5098  resima2  5099  imaeq1  5124  imaeq2  5125  dfima2  5131  nfima  5137  mptima  5141  rnresi  5147  resiima  5148  ima0  5149  imadisj  5152  imass1  5165  imass2  5166  ndmima  5167  imaundi  5203  imaundir  5204  inimass  5207  rninxp  5234  imainrect  5236  xpima1  5237  xpima2m  5238  dfrn4  5251  imacnvcnv  5255  imadmres  5283  mptpreima  5284  rnco2  5298  funcnvres  5457  funimacnv  5460  funimaexg  5468  fnima  5505  fores  5628  f1ores  5657  f1orescnv  5658  foimacnv  5660  resdif  5664  funfvima  5953  resfunexgALT  6341  smores2  6569  sbthlemi4  7282  sbthlemi6  7284  sbthlemi8  7286  djuin  7410  djuun  7413  casedm  7432  eninl  7443  eninr  7444  djudm  7451  hashf1lem1  11307  ghmima  14127  conjsubg  14139  rnrhmsubrg  14669  tgrest  15395  cnconst2  15459  hmeores  15541  fsumdvdsmul  16285