Definition df-ima 4785

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 4784) and range (df-rn 4783). For an alternate definition, see dfima2 5126. (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 4775	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4774	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4773	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1402	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is used by:  resima  5094  resima2  5095  imaeq1  5119  imaeq2  5120  dfima2  5126  nfima  5132  mptima  5136  rnresi  5142  resiima  5143  ima0  5144  imadisj  5147  imass1  5160  imass2  5161  ndmima  5162  imaundi  5198  imaundir  5199  inimass  5202  rninxp  5229  imainrect  5231  xpima1  5232  xpima2m  5233  dfrn4  5246  imacnvcnv  5250  imadmres  5278  mptpreima  5279  rnco2  5293  funcnvres  5452  funimacnv  5455  funimaexg  5463  fnima  5500  fores  5623  f1ores  5652  f1orescnv  5653  foimacnv  5655  resdif  5659  funfvima  5944  resfunexgALT  6331  smores2  6559  sbthlemi4  7271  sbthlemi6  7273  sbthlemi8  7275  djuin  7398  djuun  7401  casedm  7420  eninl  7431  eninr  7432  djudm  7439  hashf1lem1  11268  ghmima  14051  conjsubg  14063  rnrhmsubrg  14543  tgrest  15253  cnconst2  15317  hmeores  15399  fsumdvdsmul  16088