Definition df-ima 4692

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 4691) and range (df-rn 4690). For an alternate definition, see dfima2 5029. (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 4682	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4681	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4680	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1373	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4997  resima2  4998  imaeq1  5022  imaeq2  5023  dfima2  5029  nfima  5035  mptima  5039  rnresi  5044  resiima  5045  ima0  5046  imadisj  5049  imass1  5062  imass2  5063  ndmima  5064  imaundi  5100  imaundir  5101  inimass  5104  rninxp  5131  imainrect  5133  xpima1  5134  xpima2m  5135  dfrn4  5148  imacnvcnv  5152  imadmres  5180  mptpreima  5181  rnco2  5195  funcnvres  5352  funimacnv  5355  funimaexg  5363  fnima  5400  fores  5515  f1ores  5544  f1orescnv  5545  foimacnv  5547  resdif  5551  funfvima  5823  resfunexgALT  6200  smores2  6387  sbthlemi4  7069  sbthlemi6  7071  sbthlemi8  7073  djuin  7173  djuun  7176  casedm  7195  eninl  7206  eninr  7207  djudm  7214  ghmima  13645  conjsubg  13657  rnrhmsubrg  14058  tgrest  14685  cnconst2  14749  hmeores  14831  fsumdvdsmul  15507