Definition df-ima 4276

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 4275) and range (df-rn 4274). For an alternate definition, see dfima2 4588. (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 4266	. 2 class (A “ B)
4	1, 2	cres 4265	. . 3 class (A ↾ B)
5	4	crn 4264	. 2 class ran (A ↾ B)
6	3, 5	wceq 1226	1 wff (A “ B) = ran (A ↾ B)

This definition is referenced by:  resima  4561  resima2  4562  imaeq1  4581  imaeq2  4582  dfima2  4588  nfima  4594  rnresi  4600  resiima  4601  ima0  4602  imadisj  4605  imass1  4618  imass2  4619  ndmima  4620  imaundi  4654  imaundir  4655  inimass  4658  rninxp  4682  imainrect  4684  xpima1  4685  xpima2m  4686  dfrn4  4699  imacnvcnv  4703  imadmres  4731  mptpreima  4732  rnco2  4746  funcnvres  4889  funimacnv  4892  funimaexg  4900  fnima  4934  fores  5031  f1ores  5057  f1orescnv  5058  foimacnv  5060  resdif  5064  funfvima  5306  resfunexgALT  5651  smores2  5822