Definition df-ima 4552

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 4551) and range (df-rn 4550). For an alternate definition, see dfima2 4883. (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 4542	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4541	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4540	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1331	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4852  resima2  4853  imaeq1  4876  imaeq2  4877  dfima2  4883  nfima  4889  rnresi  4896  resiima  4897  ima0  4898  imadisj  4901  imass1  4914  imass2  4915  ndmima  4916  imaundi  4951  imaundir  4952  inimass  4955  rninxp  4982  imainrect  4984  xpima1  4985  xpima2m  4986  dfrn4  4999  imacnvcnv  5003  imadmres  5031  mptpreima  5032  rnco2  5046  funcnvres  5196  funimacnv  5199  funimaexg  5207  fnima  5241  fores  5354  f1ores  5382  f1orescnv  5383  foimacnv  5385  resdif  5389  funfvima  5649  resfunexgALT  6008  smores2  6191  sbthlemi4  6848  sbthlemi6  6850  sbthlemi8  6852  djuin  6949  djuun  6952  casedm  6971  eninl  6982  eninr  6983  djudm  6990  tgrest  12338  cnconst2  12402  hmeores  12484