Definition df-ima 4426

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 4425) and range (df-rn 4424). For an alternate definition, see dfima2 4745. (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 4416	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4415	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4414	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1287	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4714  resima2  4715  imaeq1  4738  imaeq2  4739  dfima2  4745  nfima  4751  rnresi  4758  resiima  4759  ima0  4760  imadisj  4763  imass1  4776  imass2  4777  ndmima  4778  imaundi  4812  imaundir  4813  inimass  4816  rninxp  4842  imainrect  4844  xpima1  4845  xpima2m  4846  dfrn4  4859  imacnvcnv  4863  imadmres  4891  mptpreima  4892  rnco2  4906  funcnvres  5054  funimacnv  5057  funimaexg  5065  fnima  5099  fores  5207  f1ores  5233  f1orescnv  5234  foimacnv  5236  resdif  5240  funfvima  5489  resfunexgALT  5840  smores2  6015  sbthlemi4  6616  sbthlemi6  6618  sbthlemi8  6620  djuun  6707  casedm  6724  djudm  6732