Definition df-ima 4281

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 4280) and range (df-rn 4279). For an alternate definition, see dfima2 4593. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-ima	⊢ (A “ B) = ran (A ↾ B)

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 4271	. 2 class (A “ B)
4	1, 2	cres 4270	. . 3 class (A ↾ B)
5	4	crn 4269	. 2 class ran (A ↾ B)
6	3, 5	wceq 1226	1 wff (A “ B) = ran (A ↾ B)

This definition is referenced by:  resima  4566  resima2  4567  imaeq1  4586  imaeq2  4587  dfima2  4593  nfima  4599  rnresi  4605  resiima  4606  ima0  4607  imadisj  4610  imass1  4623  imass2  4624  ndmima  4625  imaundi  4659  imaundir  4660  inimass  4663  rninxp  4687  imainrect  4689  xpima1  4690  xpima2m  4691  dfrn4  4704  imacnvcnv  4708  imadmres  4736  mptpreima  4737  rnco2  4751  funcnvres  4894  funimacnv  4897  funimaexg  4905  fnima  4939  fores  5036  f1ores  5062  f1orescnv  5063  foimacnv  5065  resdif  5069  funfvima  5311  resfunexgALT  5656  smores2  5827