Definition df-ima 4617

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 4616) and range (df-rn 4615). For an alternate definition, see dfima2 4948. (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 4607	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4606	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4605	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1343	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4917  resima2  4918  imaeq1  4941  imaeq2  4942  dfima2  4948  nfima  4954  rnresi  4961  resiima  4962  ima0  4963  imadisj  4966  imass1  4979  imass2  4980  ndmima  4981  imaundi  5016  imaundir  5017  inimass  5020  rninxp  5047  imainrect  5049  xpima1  5050  xpima2m  5051  dfrn4  5064  imacnvcnv  5068  imadmres  5096  mptpreima  5097  rnco2  5111  funcnvres  5261  funimacnv  5264  funimaexg  5272  fnima  5306  fores  5419  f1ores  5447  f1orescnv  5448  foimacnv  5450  resdif  5454  funfvima  5716  resfunexgALT  6076  smores2  6262  sbthlemi4  6925  sbthlemi6  6927  sbthlemi8  6929  djuin  7029  djuun  7032  casedm  7051  eninl  7062  eninr  7063  djudm  7070  tgrest  12809  cnconst2  12873  hmeores  12955