Definition df-ima 4611

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 4610) and range (df-rn 4609). For an alternate definition, see dfima2 4942. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-ima	|- ( A " B ) = ran ( A |` B )

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 4601	. 2 class ( A " B )
4	1, 2	cres 4600	. . 3 class ( A |` B )
5	4	crn 4599	. 2 class ran ( A |` B )
6	3, 5	wceq 1342	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4911  resima2  4912  imaeq1  4935  imaeq2  4936  dfima2  4942  nfima  4948  rnresi  4955  resiima  4956  ima0  4957  imadisj  4960  imass1  4973  imass2  4974  ndmima  4975  imaundi  5010  imaundir  5011  inimass  5014  rninxp  5041  imainrect  5043  xpima1  5044  xpima2m  5045  dfrn4  5058  imacnvcnv  5062  imadmres  5090  mptpreima  5091  rnco2  5105  funcnvres  5255  funimacnv  5258  funimaexg  5266  fnima  5300  fores  5413  f1ores  5441  f1orescnv  5442  foimacnv  5444  resdif  5448  funfvima  5710  resfunexgALT  6070  smores2  6253  sbthlemi4  6916  sbthlemi6  6918  sbthlemi8  6920  djuin  7020  djuun  7023  casedm  7042  eninl  7053  eninr  7054  djudm  7061  tgrest  12710  cnconst2  12774  hmeores  12856