Definition df-ima 4734

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

This definition is referenced by:  resima  5042  resima2  5043  imaeq1  5067  imaeq2  5068  dfima2  5074  nfima  5080  mptima  5084  rnresi  5089  resiima  5090  ima0  5091  imadisj  5094  imass1  5107  imass2  5108  ndmima  5109  imaundi  5145  imaundir  5146  inimass  5149  rninxp  5176  imainrect  5178  xpima1  5179  xpima2m  5180  dfrn4  5193  imacnvcnv  5197  imadmres  5225  mptpreima  5226  rnco2  5240  funcnvres  5398  funimacnv  5401  funimaexg  5409  fnima  5446  fores  5564  f1ores  5593  f1orescnv  5594  foimacnv  5596  resdif  5600  funfvima  5879  resfunexgALT  6263  smores2  6453  sbthlemi4  7148  sbthlemi6  7150  sbthlemi8  7152  djuin  7252  djuun  7255  casedm  7274  eninl  7285  eninr  7286  djudm  7293  ghmima  13839  conjsubg  13851  rnrhmsubrg  14253  tgrest  14880  cnconst2  14944  hmeores  15026  fsumdvdsmul  15702