Definition df-ima 4677

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 4676) and range (df-rn 4675). For an alternate definition, see dfima2 5012. (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 4667	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4666	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4665	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1364	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  4980  resima2  4981  imaeq1  5005  imaeq2  5006  dfima2  5012  nfima  5018  mptima  5022  rnresi  5027  resiima  5028  ima0  5029  imadisj  5032  imass1  5045  imass2  5046  ndmima  5047  imaundi  5083  imaundir  5084  inimass  5087  rninxp  5114  imainrect  5116  xpima1  5117  xpima2m  5118  dfrn4  5131  imacnvcnv  5135  imadmres  5163  mptpreima  5164  rnco2  5178  funcnvres  5332  funimacnv  5335  funimaexg  5343  fnima  5379  fores  5493  f1ores  5522  f1orescnv  5523  foimacnv  5525  resdif  5529  funfvima  5797  resfunexgALT  6174  smores2  6361  sbthlemi4  7035  sbthlemi6  7037  sbthlemi8  7039  djuin  7139  djuun  7142  casedm  7161  eninl  7172  eninr  7173  djudm  7180  ghmima  13471  conjsubg  13483  rnrhmsubrg  13884  tgrest  14489  cnconst2  14553  hmeores  14635  fsumdvdsmul  15311