Definition df-ima 4358

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 4357) and range (df-rn 4356). For an alternate definition, see dfima2 4670. (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 4348	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4347	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4346	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1243	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4643  resima2  4644  imaeq1  4663  imaeq2  4664  dfima2  4670  nfima  4676  rnresi  4682  resiima  4683  ima0  4684  imadisj  4687  imass1  4700  imass2  4701  ndmima  4702  imaundi  4736  imaundir  4737  inimass  4740  rninxp  4764  imainrect  4766  xpima1  4767  xpima2m  4768  dfrn4  4781  imacnvcnv  4785  imadmres  4813  mptpreima  4814  rnco2  4828  funcnvres  4972  funimacnv  4975  funimaexg  4983  fnima  5017  fores  5115  f1ores  5141  f1orescnv  5142  foimacnv  5144  resdif  5148  funfvima  5390  resfunexgALT  5737  smores2  5909