Definition df-ima 4378

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 4377) and range (df-rn 4376). For an alternate definition, see dfima2 4694. (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 4368	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4367	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4366	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1285	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4665  resima2  4666  imaeq1  4687  imaeq2  4688  dfima2  4694  nfima  4700  rnresi  4706  resiima  4707  ima0  4708  imadisj  4711  imass1  4724  imass2  4725  ndmima  4726  imaundi  4760  imaundir  4761  inimass  4764  rninxp  4788  imainrect  4790  xpima1  4791  xpima2m  4792  dfrn4  4805  imacnvcnv  4809  imadmres  4837  mptpreima  4838  rnco2  4852  funcnvres  4997  funimacnv  5000  funimaexg  5008  fnima  5042  fores  5140  f1ores  5166  f1orescnv  5167  foimacnv  5169  resdif  5173  funfvima  5416  resfunexgALT  5762  smores2  5937