Definition df-ima 4657

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 4656) and range (df-rn 4655). For an alternate definition, see dfima2 4990. (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 4647	. 2 class ( A " B )
4	1, 2	cres 4646	. . 3 class ( A |` B )
5	4	crn 4645	. 2 class ran ( A |` B )
6	3, 5	wceq 1364	1 wff ( A " B ) = ran ( A |` B )

This definition is referenced by:  resima  4958  resima2  4959  imaeq1  4983  imaeq2  4984  dfima2  4990  nfima  4996  rnresi  5003  resiima  5004  ima0  5005  imadisj  5008  imass1  5021  imass2  5022  ndmima  5023  imaundi  5059  imaundir  5060  inimass  5063  rninxp  5090  imainrect  5092  xpima1  5093  xpima2m  5094  dfrn4  5107  imacnvcnv  5111  imadmres  5139  mptpreima  5140  rnco2  5154  funcnvres  5308  funimacnv  5311  funimaexg  5319  fnima  5353  fores  5466  f1ores  5495  f1orescnv  5496  foimacnv  5498  resdif  5502  funfvima  5769  resfunexgALT  6133  smores2  6319  sbthlemi4  6989  sbthlemi6  6991  sbthlemi8  6993  djuin  7093  djuun  7096  casedm  7115  eninl  7126  eninr  7127  djudm  7134  ghmima  13204  conjsubg  13216  tgrest  14129  cnconst2  14193  hmeores  14275