Definition df-ima 4744

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 4743) and range (df-rn 4742). For an alternate definition, see dfima2 5084. (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 4734	. 2 class (𝐴 “ 𝐵)
4	1, 2	cres 4733	. . 3 class (𝐴 ↾ 𝐵)
5	4	crn 4732	. 2 class ran (𝐴 ↾ 𝐵)
6	3, 5	wceq 1398	1 wff (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵)

This definition is referenced by:  resima  5052  resima2  5053  imaeq1  5077  imaeq2  5078  dfima2  5084  nfima  5090  mptima  5094  rnresi  5100  resiima  5101  ima0  5102  imadisj  5105  imass1  5118  imass2  5119  ndmima  5120  imaundi  5156  imaundir  5157  inimass  5160  rninxp  5187  imainrect  5189  xpima1  5190  xpima2m  5191  dfrn4  5204  imacnvcnv  5208  imadmres  5236  mptpreima  5237  rnco2  5251  funcnvres  5410  funimacnv  5413  funimaexg  5421  fnima  5458  fores  5578  f1ores  5607  f1orescnv  5608  foimacnv  5610  resdif  5614  funfvima  5896  resfunexgALT  6279  smores2  6503  sbthlemi4  7202  sbthlemi6  7204  sbthlemi8  7206  djuin  7323  djuun  7326  casedm  7345  eninl  7356  eninr  7357  djudm  7364  ghmima  13932  conjsubg  13944  rnrhmsubrg  14347  tgrest  14980  cnconst2  15044  hmeores  15126  fsumdvdsmul  15805