Definition df-ima 4633

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 4632) and range (df-rn 4631). For an alternate definition, see dfima2 4965. (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 4623	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4622	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4621	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1353	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4933  resima2  4934  imaeq1  4958  imaeq2  4959  dfima2  4965  nfima  4971  rnresi  4978  resiima  4979  ima0  4980  imadisj  4983  imass1  4996  imass2  4997  ndmima  4998  imaundi  5033  imaundir  5034  inimass  5037  rninxp  5064  imainrect  5066  xpima1  5067  xpima2m  5068  dfrn4  5081  imacnvcnv  5085  imadmres  5113  mptpreima  5114  rnco2  5128  funcnvres  5281  funimacnv  5284  funimaexg  5292  fnima  5326  fores  5439  f1ores  5468  f1orescnv  5469  foimacnv  5471  resdif  5475  funfvima  5739  resfunexgALT  6099  smores2  6285  sbthlemi4  6949  sbthlemi6  6951  sbthlemi8  6953  djuin  7053  djuun  7056  casedm  7075  eninl  7086  eninr  7087  djudm  7094  tgrest  13240  cnconst2  13304  hmeores  13386