Definition df-ima 4764

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 4763) and range (df-rn 4762). For an alternate definition, see dfima2 5105. (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 4754	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4753	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4752	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1398	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5073  resima2  5074  imaeq1  5098  imaeq2  5099  dfima2  5105  nfima  5111  mptima  5115  rnresi  5121  resiima  5122  ima0  5123  imadisj  5126  imass1  5139  imass2  5140  ndmima  5141  imaundi  5177  imaundir  5178  inimass  5181  rninxp  5208  imainrect  5210  xpima1  5211  xpima2m  5212  dfrn4  5225  imacnvcnv  5229  imadmres  5257  mptpreima  5258  rnco2  5272  funcnvres  5431  funimacnv  5434  funimaexg  5442  fnima  5479  fores  5602  f1ores  5631  f1orescnv  5632  foimacnv  5634  resdif  5638  funfvima  5920  resfunexgALT  6303  smores2  6527  sbthlemi4  7232  sbthlemi6  7234  sbthlemi8  7236  djuin  7357  djuun  7360  casedm  7379  eninl  7390  eninr  7391  djudm  7398  ghmima  13999  conjsubg  14011  rnrhmsubrg  14414  tgrest  15051  cnconst2  15115  hmeores  15197  fsumdvdsmul  15876