Definition df-ima 4657

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 4656) and range (df-rn 4655). For an alternate definition, see dfima2 4990. (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 4647	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4646	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4645	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1364	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4958  resima2  4959  imaeq1  4983  imaeq2  4984  dfima2  4990  nfima  4996  rnresi  5003  resiima  5004  ima0  5005  imadisj  5008  imass1  5021  imass2  5022  ndmima  5023  imaundi  5059  imaundir  5060  inimass  5063  rninxp  5090  imainrect  5092  xpima1  5093  xpima2m  5094  dfrn4  5107  imacnvcnv  5111  imadmres  5139  mptpreima  5140  rnco2  5154  funcnvres  5308  funimacnv  5311  funimaexg  5319  fnima  5353  fores  5466  f1ores  5495  f1orescnv  5496  foimacnv  5498  resdif  5502  funfvima  5769  resfunexgALT  6134  smores2  6320  sbthlemi4  6990  sbthlemi6  6992  sbthlemi8  6994  djuin  7094  djuun  7097  casedm  7116  eninl  7127  eninr  7128  djudm  7135  ghmima  13221  conjsubg  13233  tgrest  14146  cnconst2  14210  hmeores  14292