Definition df-ima 4640

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 4639) and range (df-rn 4638). For an alternate definition, see dfima2 4973. (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 4630	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4629	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4628	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1353	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4941  resima2  4942  imaeq1  4966  imaeq2  4967  dfima2  4973  nfima  4979  rnresi  4986  resiima  4987  ima0  4988  imadisj  4991  imass1  5004  imass2  5005  ndmima  5006  imaundi  5042  imaundir  5043  inimass  5046  rninxp  5073  imainrect  5075  xpima1  5076  xpima2m  5077  dfrn4  5090  imacnvcnv  5094  imadmres  5122  mptpreima  5123  rnco2  5137  funcnvres  5290  funimacnv  5293  funimaexg  5301  fnima  5335  fores  5448  f1ores  5477  f1orescnv  5478  foimacnv  5480  resdif  5484  funfvima  5749  resfunexgALT  6109  smores2  6295  sbthlemi4  6959  sbthlemi6  6961  sbthlemi8  6963  djuin  7063  djuun  7066  casedm  7085  eninl  7096  eninr  7097  djudm  7104  tgrest  13672  cnconst2  13736  hmeores  13818