Definition df-ima 4767

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 4766) and range (df-rn 4765). For an alternate definition, see dfima2 5108. (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 4757	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4756	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4755	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1398	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5076  resima2  5077  imaeq1  5101  imaeq2  5102  dfima2  5108  nfima  5114  mptima  5118  rnresi  5124  resiima  5125  ima0  5126  imadisj  5129  imass1  5142  imass2  5143  ndmima  5144  imaundi  5180  imaundir  5181  inimass  5184  rninxp  5211  imainrect  5213  xpima1  5214  xpima2m  5215  dfrn4  5228  imacnvcnv  5232  imadmres  5260  mptpreima  5261  rnco2  5275  funcnvres  5434  funimacnv  5437  funimaexg  5445  fnima  5482  fores  5605  f1ores  5634  f1orescnv  5635  foimacnv  5637  resdif  5641  funfvima  5923  resfunexgALT  6310  smores2  6538  sbthlemi4  7243  sbthlemi6  7245  sbthlemi8  7247  djuin  7368  djuun  7371  casedm  7390  eninl  7401  eninr  7402  djudm  7409  ghmima  14018  conjsubg  14030  rnrhmsubrg  14498  tgrest  15160  cnconst2  15224  hmeores  15306  fsumdvdsmul  15985