Definition df-ima 4732

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 4731) and range (df-rn 4730). For an alternate definition, see dfima2 5070. (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 4722	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4721	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4720	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1395	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5038  resima2  5039  imaeq1  5063  imaeq2  5064  dfima2  5070  nfima  5076  mptima  5080  rnresi  5085  resiima  5086  ima0  5087  imadisj  5090  imass1  5103  imass2  5104  ndmima  5105  imaundi  5141  imaundir  5142  inimass  5145  rninxp  5172  imainrect  5174  xpima1  5175  xpima2m  5176  dfrn4  5189  imacnvcnv  5193  imadmres  5221  mptpreima  5222  rnco2  5236  funcnvres  5394  funimacnv  5397  funimaexg  5405  fnima  5442  fores  5560  f1ores  5589  f1orescnv  5590  foimacnv  5592  resdif  5596  funfvima  5875  resfunexgALT  6259  smores2  6446  sbthlemi4  7135  sbthlemi6  7137  sbthlemi8  7139  djuin  7239  djuun  7242  casedm  7261  eninl  7272  eninr  7273  djudm  7280  ghmima  13810  conjsubg  13822  rnrhmsubrg  14224  tgrest  14851  cnconst2  14915  hmeores  14997  fsumdvdsmul  15673