Definition df-ima 4738

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 4737) and range (df-rn 4736). For an alternate definition, see dfima2 5078. (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 4728	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4727	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4726	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1397	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5046  resima2  5047  imaeq1  5071  imaeq2  5072  dfima2  5078  nfima  5084  mptima  5088  rnresi  5093  resiima  5094  ima0  5095  imadisj  5098  imass1  5111  imass2  5112  ndmima  5113  imaundi  5149  imaundir  5150  inimass  5153  rninxp  5180  imainrect  5182  xpima1  5183  xpima2m  5184  dfrn4  5197  imacnvcnv  5201  imadmres  5229  mptpreima  5230  rnco2  5244  funcnvres  5403  funimacnv  5406  funimaexg  5414  fnima  5451  fores  5569  f1ores  5598  f1orescnv  5599  foimacnv  5601  resdif  5605  funfvima  5885  resfunexgALT  6269  smores2  6459  sbthlemi4  7158  sbthlemi6  7160  sbthlemi8  7162  djuin  7262  djuun  7265  casedm  7284  eninl  7295  eninr  7296  djudm  7303  ghmima  13851  conjsubg  13863  rnrhmsubrg  14265  tgrest  14892  cnconst2  14956  hmeores  15038  fsumdvdsmul  15714